Proof of A Cluster Point of a Sequence in a Metric Space is the Limit of a Subsequence

Properties of the order on $\mathbb{N}$ are those of Properties of the Order on the Natural Numbers, and $m+1=S(m)$ for the successor map $S$ is claim 1 of Arithmetic of Addition on the Natural Numbers.

Claim 1. We define $(n_k)_{k\in\mathbb{N}}$ by recursion on the natural numbers, at each step taking a least witness, so that no choice principle is used.

Base. Let $A_1=\{m\in\mathbb{N}:d(x_m,x)<\varepsilon_1\}$. Applying Cluster Point of a Sequence in a Metric Space with the real number $\varepsilon_1>0$ and with $N=1$ produces $m\in\mathbb{N}$ with $1\le m$ and $d(x_m,x)<\varepsilon_1$, so $A_1$ is nonempty. Set $n_1=\min A_1$, which exists by The Natural Numbers Are Well Ordered.

Step. Suppose $n_k\in\mathbb{N}$ has been defined. Let

Applying Cluster Point of a Sequence in a Metric Space with the real number $\varepsilon_{k+1}>0$ and with $N=n_k+1$ produces $m\in\mathbb{N}$ with $n_k+1\le m$ and $d(x_m,x)<\varepsilon_{k+1}$. Since $n_k<n_k+1$ by claim 6 of Properties of the Order on the Natural Numbers, and $n_k+1\le m$ means $n_k+1=m$ or $n_k+1<m$, transitivity of $<$ (claim 1) gives $n_k<m$ in either case. Hence $A_{k+1}$ is nonempty, and we set $n_{k+1}=\min A_{k+1}$, again by The Natural Numbers Are Well Ordered.

By construction $n_{k+1}\in A_{k+1}$, so $n_k<n_{k+1}$ for every $k\in\mathbb{N}$; thus $(n_k)_{k\in\mathbb{N}}$ is strictly increasing in the sense of Subsequence of a Sequence in a Set. Also $n_1\in A_1$ gives $d(x_{n_1},x)<\varepsilon_1$, and $n_{k+1}\in A_{k+1}$ gives $d(x_{n_{k+1}},x)<\varepsilon_{k+1}$, so $d(x_{n_k},x)<\varepsilon_k$ for every $k\in\mathbb{N}$ by the principle of induction. This proves claim 1.

Claim 2. Let $(n_k)_{k\in\mathbb{N}}$ be strictly increasing with $d(x_{n_k},x)<\varepsilon_k$ for every $k$, and assume $(\varepsilon_k)_{k\in\mathbb{N}}$ has limit $0$. Let $\varepsilon$ be a real number with $0<\varepsilon$. By Limit of a Sequence of Real Numbers there is $K\in\mathbb{N}$ such that $|\varepsilon_k-0|<\varepsilon$ for every $k\in\mathbb{N}$ with $K\le k$. By claim 4 of Additive Cancellation and Elementary Additive Identities in a Field we have $\varepsilon_k-0=\varepsilon_k$, and since $0<\varepsilon_k$ the absolute value satisfies $|\varepsilon_k|=\varepsilon_k$. Hence $\varepsilon_k<\varepsilon$ whenever $K\le k$.

Now let $k\in\mathbb{N}$ with $K\le k$. Then $d(x_{n_k},x)<\varepsilon_k$ and $\varepsilon_k<\varepsilon$, so transitivity of $<$ in an ordered field, as recorded in claim 2 of Elementary Order Arithmetic in an Ordered Field, gives $d(x_{n_k},x)<\varepsilon$. Since $\varepsilon>0$ was arbitrary, Convergent Sequence in a Metric Space shows that the sequence $(x_{n_k})_{k\in\mathbb{N}}$ converges to $x$ in $(X,d)$.