Is there a constructive proof of this characterisation of convergence of sequences? The following is a useful characterisation of convergence for sequences in $\mathbb R$:

A sequence $(a_n)$ converges to $a$ if and only if every subsequence $(a_{n_k})$ of $(a_n)$ has a subsequence $(a_{n_{k_\ell}})$ converging to $a$. 

The usual proof of this statement is very short. If $(a_n)$ converges to $a$, it is immediate that every subsequence does so, and each of their subsequences also converges to $a$. Conversely, suppose $(a_n)$ does not converge to $a$. This means there exists $\varepsilon > 0$ such that for every $N > 0$, there exists $n > N$ with $|a_n - a| \geq \varepsilon$. These $a_n$ for a subsequence with no further subsequences converging to $a$, so by the contrapositive, we are done.
However, the second part of the proof says that the "negation is false" rather than saying that "the result is true". Proving that the negation is false is easy because we can rather concretely construct a subsequence that fails, but my attempts to give a direct proof have never been fruitful. Does anyone know any direct proofs of this fact?
 A: You can convert the contrapositive argument to a direct proof by transfinite recursion.
Fix $\epsilon>0$ and consider the set $A=\{n\in\mathbb{N}: |a_n-a|<\epsilon \}$. We want to prove that the complement $\mathbb{N}\setminus A$ is finite by constructing larger and larger subsets $A_\alpha\subset A$ for ordinals $\alpha$. If at any point in the construction we reach a set $A_\alpha\subset A$ such that $\mathbb{N}\setminus A_\alpha$ is finite, then also $\mathbb{N}\setminus A$ is finite and we are done.
We start the recursion from the empty set $A_0=\emptyset$.
For transfinite recursion we need to define two ways to extend the set. 


*

*For successor ordinals $\alpha+1$, if $\mathbb{N}\setminus A_\alpha$ is not finite we may consider the sequence $(a_n)_{n\in \mathbb{N}\setminus A_\alpha}$. By assumption this sequence has a subsequence $a_{n_k}$ converging to $a$. In particular, the tail of the subsequence gives indices $n_k\in A\setminus A_\alpha$. Let $A_{\alpha+1}$ be the set obtained by extending $A_\alpha$ by these points.

*For limit ordinals $\alpha$, we define $A_\alpha = \bigcup_{\beta<\alpha}A_\beta$.


For any ordinal $\alpha$ that this construction reaches, we may define an injection $\alpha\to A_\alpha$ by considering the new points added in each step of the construction. On the other hand since $A_\alpha\subset\mathbb{N}$ and there are no injections $\alpha\to\mathbb{N}$ when $\alpha$ has cardinality bigger than the integers, we know the construction must eventually terminate.
A: Assume that every subsequence of $(a_n)$ has an own subsequence converging to $a$.
We show the convergence of $(a_n)$ using the definition.
Let $\epsilon>0$.


*

*If there are only finitely many terms of $(a_n)$ outside $I_\epsilon=(a-\epsilon,a+\epsilon)$ we can find that $N_\epsilon$...

*Else, there are infinitely many terms of $(a_n)$ outside $I_\epsilon$. We pick a subsequence of $(a_n)$ that stays outside $I_\epsilon$. From the given property, it has an own subsequence converging to $a$, so this own subsequence will land inside $I_\epsilon$ after some index (entirely). Contradiction. This else block is false.



I hope that the used proof by contradiction happens to a deeper, acceptable level.
