Proving there is a sequence convergent to a limit point of a set without axiom of countable choice? Often, we use a construction like this: Given a subset $ A $ of a metric space and its limit point $ a $, we know that for every $ \epsilon > 0 $ there is another point $ x $  different from $ a $ such that $ d(x,a) < \epsilon $. So for every natural $ n $ we let $ a_n $ be such a point within $ 1/n $ of $ a $, which gives us a sequence convergent to $ a $.
My question is, is the axiom of countable choice needed for this construction, or is it formally correct just in ZF?
 A: This result is not provable in ZF.  Cohen's original model for the failure of the axiom of choice satisfies the statement "There is a dense subset $D$ of the real line such that any sequence $(a_n)_{n\in\mathbb N}$ of elements of $D$ has only finitely many distinct elements."
A: Not only that the result is not provable in $\sf ZF$ itself. If we allow general metric spaces, then this is in fact equivalent to the axiom of countable choice.
Given a countable family non-empty sets, $X_n$, and let $A_n=\prod_{k\leq n}X_k$. If we can choose $a_n\in A_n$ then we can define a choice function from the $X_n$'s as well by defining $x_n=a_n(n)$ (recall that $a_n$ is a choice function). In fact, even if we can only choose from an infinite subset $I$ of the $A_n$'s we are done, by defining $k(n)=\min\{k\in I\mid n\leq k\}$ and taking $x_n=a_{k(n)}(n)$.
Consider $A$ to be the space whose underlying set is $\bigcup A_n\cup\{\infty\}$, where $\infty$ is a point which is not in any of the $A_n$'s. We define the metric to be as follows: $$d(x,y)=\begin{cases}0 & x=y\\\frac1n & x=\infty,y\in A_n\\\frac1n & x\in A_n,y=\infty \\ 1 & x\neq y,x\neq\infty,y\neq\infty\end{cases}$$
Clearly $\infty$ is an accumulation point of $\bigcup A_n$, therefore there exists a sequence $r_n$ such that $d(r_n,\infty)\to0$. But this concludes the proof, because a sequence converging to $\infty$ must pass through infinitely many of the $A_n$'s, therefore we can define $k(n)=\min\{k\mid r_k\in A_n\}$ and then we can take $a_n=r_{k(n)}$, where it is a well-defined choice, and this is a choice from infinitely many of the $A_n$'s, therefore it defines a choice from the family of the $X_n$'s from which we originally started.
