(ZF) Prove 'the set of all subsequential limits of a sequence in a metric space is closed. Let $X$ be a metric space.
Let $\{p_n\}$ be a sequence in $X$.
Let $E$ be a set of all subsequential limits of $\{p_n\}$.
How do i prove that $E$ is closed in ZF?
Is there a well-ordering of convergent subsequences? I can't think of one..
 A: Let us denote $\{ p_n : n \in \mathbb{N} \}$ by $B$.
Clearly $x \in \overline{ B }$ iff $x = p_n$ for some $n$, or $( \forall m ) ( \exists n ) ( 0 < d (x,p_n ) \leq \frac{1}{m} )$.  In the latter case we can construct, via induction and without any choice, a subsequence converging to $x$.  (In fact, the latter condition is easily seen to be equivalent to $x$ being a subsequential limit of $(p_n)_{n \in \mathbb{N}}$.)
Suppose $x \in \overline{ B }$ is not a subsequential limit.  This means that $x = p_n$ for some $n$.  But also that there is an $m \in \mathbb{N}$ such that $d ( x , p_n ) > \frac{1}{m}$ for all $n$.  Therefore $x$ is an isolated point of $B$, and thence it is also an isolated point of $\overline{ B }$.
It thus suffices to show that $\overline{ B } \setminus \{ x : x\text{ is an isolated point of }B \}$ is closed, and this follows from the following:
Claim:  Suppose $F \subseteq X$ is closed and $A \subseteq F$ is a set of isolated points of $F$.  Then $F \setminus A$ is closed.  
Proof:  It suffices to show that $X \setminus ( F \setminus A)$ is open.  If $x \in X \setminus ( F \setminus A )$ there are two cases:  Either $x \notin F$, in which case $x \in X \setminus F$, and this is a neighbourhood of $x$ disjoint from $F \setminus A$.  Otherwise $x \in A$, but as $x$ is isolated there is a neighbourhood $U$ of $x$ such that $F \cap U = \{ x \}$, and therefore $( F \setminus A ) \cap U = \emptyset$.) $\dashv$
Edit:  There is a minor issue in what I have done above.  I seem to have assumed that the sequence $( p_n )_{n \in \mathbb{N}}$ is one-to-one (silly me).  This means that some of what I said above is not quite true in general.  The relevant facts we still have are:


*

*If $x \in \overline{B}$ then either $x \in B$ or there is a subsequence of $( p_n )_{n \in \mathbb{N}}$ converging to $a$.

*If there is a subsequence of $( p_n )_{n \in \mathbb{N}}$ converging to $x$, then either $( \forall m ) ( \exists n ) ( 0 < d (x,p_n ) \leq \frac{1}{m} )$, or $( \forall N ) ( \exists n \geq N ) ( p_n = x )$.


The set we wish to show is closed is therefore $\overline{B} \setminus A$ where $$A = \{ x \in B : x\text{ is an isolated point of }A\text{ and }( \exists N ) ( \forall n \geq N ) ( p_n \neq x ) \}.$$  As $A$ is a set of isolated points, by the above $\overline{B} \setminus A$ is closed.
A: Check if this is ok: $ \forall $ $ y $ in the closure of $ E $, let $ N_{y} $ be any neighbourhood of $ y $. Then, by definition of an element of the closure, for any neighbourhood of $ y $, $ N_{y} \bigcap E \neq \emptyset $.
By the same token, for any z in E, $ N_{z} $ (any neighbourhood of z) is such that $ N_{z} \bigcap \left(p_{n}\right) \neq \emptyset $.
Therefore, there is a $ z \in  N_{y} \bigcap E $ so that $ N_{z} \bigcap \left(p_{n}\right) \neq \emptyset $.
Let $ N = N_{z} \bigcap N_{y} $. Then N is a neighbourhood of z and $ N \subset N_{y} $ (intersections of neighbourhoods are neighbourhoods and z is in both)
Therefore $ N_{y} \bigcap \left(p_{n}\right) \neq \emptyset $. And $ y $ is in $ E $, so that $ E $ is closed, since $ N_{y} $ is arbitrary
Since in this construction there are only intersections of sets, I think it is independent from AC.
A: How about my proof? 
proof: Let $(p_n)$ be a sequence in metric space $X.$
    If $q\in X$ is a subsequential limit of sequence $(p_n),$  then there exists a subsequence $(p_{\sigma_q(m)})_{m\in\mathbb{N}}$ of $(p_n),$ such that $\lim\limits_{m\to\infty} p_{\sigma_{q}(m)}=q,$ where $\sigma_{q} : \mathbb{N}\to\mathbb{N}$ is increasing strictly. Put  $$E=\{q\in X\mid \exists \text{ subsequence }(p_{\sigma_q(m)})_{m\in\mathbb{N}} \text{ of $(p_n)_{n\in\mathbb{N}}$ } :  \lim\limits_{m\to\infty} p_{\sigma_q(m)}=q \}.$$   To show $E$ is closed, let $x\in E',$ and we shall prove that $x\in E.$  
For $n=1,$ since $\hat{\mathbb{B}}(x,\frac{1}{2\cdot 1})\cap E\neq\emptyset,$ pick $q_1\in\hat{\mathbb{B}}(x,\frac{1}{2\cdot 1})\cap E,$ then $q_1\in E$ and $d(q_1,x)<\frac{1}{2}.$ Hence there exists subsequence $(p_{\sigma_1(m)})_{m\in\mathbb{N}}$ such that $\lim_{m\to\infty} p_{\sigma_1(m)}=q_1.$  Hence there exists $M_1\in\mathbb{N}$ such that for all $m\geq M_1, d(p_{\sigma_1(m)}, q_1)<\frac{1}{2},$ 
thus $ d(x,p_{\sigma_1(M_1)})\leq d(x,q_1)+d(q_1, p_{\sigma_1(M_1)})<1.$
For $n=2,$ since $\hat{\mathbb{B}}(x,\frac{1}{2\cdot 2})\cap E\neq\emptyset,$ pick $q_2\in\hat{\mathbb{B}}(x,\frac{1}{2\cdot 2})\cap E,$ then $q_2\in E$ and $d(q_2,x)<\frac{1}{2\cdot 2}.$ Hence there exists subsequence $(p_{\sigma_2(m)})_{m\in\mathbb{N}}$ such that 
    $\lim_{m\to\infty} p_{\sigma_2(m)}=q_2.$  Hence there exists $M_2\in\mathbb{N}$ with $M_2>\sigma_1(M_1)$ such that for all $m\geq M_2,$  $d(p_{\sigma_2(m)}, q_2)<\frac{1}{2\cdot 2},$ thus $$d(x,p_{\sigma_2(M_2)})\leq d(x,q_2)+d(q_2, p_{\sigma_2(M_2)})<\frac{1}{2}$$ and $\sigma_2(M_2)\geq M_2>\sigma_1(M_1)$ (note that $\sigma_2$ is increasing strictly).
    Now assume we have constructed $p_{\sigma_1(M_1)}, \dots, p_{\sigma_k(M_k)},$ such that 
    \begin{gather*}
 d(x, p_{\sigma_i(M_i)})<\frac{1}{i}, \qquad \forall i=1,\dots,k 
 \end{gather*}
    with $\sigma_1(M_1)<\cdots<\sigma_{k}(M_k).$ 
    As for $n=k+1,$
     Since $x\in E',$     $\hat{\mathbb{B}}(x,\frac{1}{2(k+1)})\cap E\neq\emptyset.$  Pick $q_{k+1}\in \hat{\mathbb{B}}(x,\frac{1}{2(k+1)})\cap E,$ then $q_{k+1}\in E$ with 
    $d(q_{k+1}, x)<\frac{1}{2(k+1)}.$   Hence there exists subsequence $(p_{\sigma_{k+1}(m)})_{m\in\mathbb{N}}$ such that $\lim\limits_{m\to\infty} p_{\sigma_{k+1}(m)}=q_{k+1}.$  Hence,   there exists $M_{k+1}\in\mathbb{N}$ with $M_{k+1}>\sigma_{k}(M_k)$ such that for all $m\geq M_{k+1},$  $d(p_{\sigma_{k+1}(m)}, q_{k+1})<\frac{1}{2(k+1)}.$ 
    Thus
    \begin{gather*}
 d(x,p_{\sigma_{k+1}(M_{k+1})})\leq d(x,q_{k+1})+d(q_{k+1}, p_{\sigma_{k+1}(M_{k+1})})<\frac{1}{k+1}, 
 \end{gather*}
    with $\sigma_{k+1}(M_{k+1})\geq M_{k+1}>\sigma_{k}(M_k).$
    Hence,  let $\eta: i\mapsto\sigma_i(M_i)\in \{p_n\mid n\in\mathbb{N}\}, \forall i\in\mathbb{N},$ then
     the mapping $\eta : \mathbb{N}\to\mathbb{N} $ is increasing strictly,   and  the principle of induction follows  that we have constructed  a subsequence $(p_{\eta(n)})_{n\in\mathbb{N}},$ such that 
     \begin{gather*}
   d(x,p_{\eta(n)})<\frac{1}{n},\qquad \forall n\in\mathbb{N}
  \end{gather*}
     holds. Since $1/n\to 0, $ as $n\to\infty, $ we see that $\lim\limits_{n\to\infty} p_{\eta(n)}=x,$ hence $x\in E.$   Since $x$ is chosen arbitrary, we conclude that  $E$ is closed.
Note that we write $\mathbb{B}(x,r):=\{y\in X\mid d(x,y)<r\}$ and $\hat{\mathbb{B}}(x,r)=\mathbb{B}(x,r)\backslash\{x\}.$
