Does this proof of $x\in E'\rightarrow \exists \{x_n\}\subseteq E : x_n\to x$ use the axiom of choice?

Question

Let $(X,d)$ be a metric space. Let $E$ be a subset of $X$.

If $x$ is a limit point of $E$, then there exists a sequence $x_n\in E$, $n= 1,2,\dots$ such that $x_n\to x$.

Proof.

Pick $x_1\in E$ such that $d(x_1,x)<1$. Having chosen $x_1,\dots,x_{n-1}$ pick $x_n\in E$ such that $x_n\neq x_k\,(k=1,\dots,n-1)$ and $d(x_n,x)<\frac 1 n$. This is possible because every open ball around $x$ has infinitely many points of $E$. It's clear that $x_n\to x$.

My question is: We're choosing points $x_i$ from sets $B_i$, does this require the axiom of choice to be justified?

Answer 1

Yes. It does.

In Cohen's first model where the axiom of choice fails (see Jech "The Axiom of Choice", Ch. 5) there exists a subset $D$ of $\Bbb R$ which is:

1. Dense.
2. Does not have any countable infinite subset.

Take any point in $\Bbb R\setminus D$, then it is in the closure of $D$ but there is no sequence in $D$ converging to it. Simply because any convergent sequence from $D$ is eventually constant.

Moreover, the statement that in a metric space a closure is the same as the sequential closure is in fact equivalent to the axiom of countable choice. See Proof of a basic $AC_\omega$ equivalence for more details.