If a metric space has the limit point property, is it separable? (ZF + AC$_\omega$) 
If a metric space has the limit point property, is it separable? (ZF + AC$_\omega$)

I'm struggling with this problem for a week.
I'm talking about this in Metric space.
Here's the part of argument in Rudin PMA p.45;
Let $X$ be limit point compact. Fix $\epsilon>0$ and $x_0 \in X$. Having chosen $x_0,\ldots,x_j \in X$, choose $x_{j+1}$, if possible, so that $d(x_i,x_{j+1})≧\epsilon$ for $i=0,\ldots,j$. Then this process must stop after a finite number of steps.
Here, Dependent Choice is used.
I know that ‘Limit point property $\Rightarrow$ separable’ is unprovable in ZF.
(You can see this: If every infinite subset has a limit point in a metric space $X$, then $X$ is separable (in ZF))
I want to prove this in ZF+AC$_\omega$. Help.
So far, I proved that [Limit point compact $\Rightarrow$ separable] $\Rightarrow$ [Limit point compact $\Rightarrow$ Compact].
I need this to complete my proof.
 A: Countable choice is sufficient. Separability is an easy consequence of total boundedness. Suppose that $X$ is not totally bounded. Then there is an $r>0$ such that for each $n\in\Bbb Z^+$, 
$$X_n=\left\{\langle x_1,\dots,x_n\rangle\in X^n:d(x_i,x_j)\ge r\text{ for }1\le i<j\le n\right\}\ne\varnothing\;.$$
By countable choice there is some $\langle a_n:n\in\Bbb Z^+\rangle\in\prod_nX_n$. For $n\in\Bbb Z^+$ let $a_n=\langle x^n_i,\dots,x^n_n\rangle$. Now concatenate the $a_n$ to form an infinite sequence
$$\sigma=\langle x^1_1,x^2_1,x^2_2,x^3_1,x^3_2,x^3_4,\dots\rangle$$
in $X$. Note that if $1\le k\le m<n$, there is at most one $s\in\{1,\dots,n\}$ such that $d(x^m_k,x^n_s)<\frac{r}2$: this is an easy consequence of the triangle inequality and the fact that the points $x^n_1,\dots,x^n_n$ are mutually at least $r$ apart.
For $n\in\Bbb Z^+$ let $B_n=\{x^n_1,\dots,x^n_n\}$. Let $y_1=x^1_1$. Suppose that $n\in\Bbb Z^+$ and that we’ve chosen $y_k\in B_k$ for $1\le k\le n$ so that the points $y_1,\dots,y_n$ are mutually at least $r/2$ apart. For $k=1,\dots,n$ let $A_k=\varnothing$ if $d(y_k,x)\ge r/2$ for each $x\in B_{n+1}$, and let $A_k=\{x\}$ if $x$ is the unique member of $B_k$ whose distance from $y_k$ is less than $r/2$. Let $A=\bigcup_{k=1}^nA_k$; clearly $|A|\le n$, so $B_{n+1}\setminus A\ne\varnothing$, and we may set $y_{n+1}=x^{n+1}_k$, where $k$ is minimal such that $x^{n+1}_k\notin A$. (Note that this choice of $y_{n+1}$ is well-defined and does not require any part of the axiom of choice.) Then $d(y_{n+1},y_k)\ge r/2$ for $k=1,\dots,n$, and the construction goes through to produce an infinite sequence $\langle y_n:n\in\Bbb Z^+\rangle$ whose terms are mutually at least $r/2$ apart.
But then the set $\{y_n:n\in\Bbb Z^+\}$ is an infinite subset of $X$ with no limit point.
A: Countable choice implies that a metric space is limit point compact if and only if it is compact. 
From there it is not hard to deduce separability, as in ZFC. 

$\newcommand{AC}{\mathsf{AC}}$
Let me point out some key points in a way for a proof of the above.
First we observe that under $\AC_\omega$ every infinite set has a countable subset. Let us see that it also implies that "every infinite set has an accumulation point" implies that every infinite sequence has a convergent subsequence:
Suppose that $\{x_n\mid n\in\omega\}$ is an infinite sequence. It has an accumulation point by the assumption. Namely a point $x$ such that for every open neighborhood $U$, there is some $x_n\neq x$ such that $x_n\in U$. Since we are in a metric space, without loss of generality this means that for every $k$ there is some $x_n\in B(x,\frac1k)$ and $x\neq x_n$.
Assume that $x\neq x_n$ for all $n$, just for simplicity, now it is clear that in every $B(x,\frac1k)$ there are infinitely many points from the sequence, otherwise there were only $m$ many points in $B(x,\frac1k)$ for some $k$, and we could then take $k'>k$ to be large enough so that none of these points appear in $B(x,\frac1{k'})$.
Since we have infinitely many, let $x_{n_k}$ be such that $n_k = \min\{n\mid x_n\in B(x,\frac1k)\}$. Note that if $k>j$ then $n_k\geq n_j$ since $x_{n_k}$ is closer to $x$ than $x_{n_j}$. If there are repetitions we can remove them by induction. We don't use the axiom of choice at all here, since this is already a well-ordered set.
Now it is not hard to see that $x_{n_k}\to x$, since for every $\varepsilon>0$ there exists $K$ such that for $k>K$ we have $x_{n_k}\in B(x,\varepsilon)$.

Conclusion I: $X$ is sequentially compact. Now let us show that it is compact.

The implication now is as in Brian's answer.
A: Suppose this process never stops and you generate a sequence $\{x_n\}$ so $d(x_k, x_l) \ge \epsilon$ for all $k$ and $l$.  Then such a sequence cannot have a convergent subsequence; it is a discrete subset of $X$.  This contradicts the limit point compactness of $X$.
