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?
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 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.