Recursive use of the Axiom of Choice In a standard proof that any sequence-compact metric space $(X,d)$ has a (finite) $\varepsilon$-net, the approach is the following: Make a sequence $(x_n)$ such that
$$
x_{n+1}\notin\bigcup_{i=1}^n B_\varepsilon(x_i)
$$
for all $n$, where $B_r(y)$ is the open ball of radius $r > 0$ around $y\in X$. Then prove that $(x_n)$ has no convergent subsequence.
The question is: Can we be sure that we can choose such a sequence? It is obvious that we must somehow make use of the Axiom of Choice, but in my opinion, it is not at all obvious that you can use that axiom recursively like this.
 A: You don’t even need the full axiom of choice for this argument: the axiom of dependent choice ($\mathsf{DC}$) is sufficient. 
Given $\epsilon>0$, let $\Sigma$ be the set of all finite sequences $\sigma$ in $X$ such that if $\sigma=\langle x_0,\ldots,x_{n-1}\rangle$, then
$$x_k\notin\bigcup_{\ell<k}B_\epsilon(x_\ell)$$
for each $k<n$. Define a relation $R$ on $\Sigma$ by $\sigma\mathrel{R}\tau$ if and only if $\sigma$ is a proper initial segment of $\tau$ (equivalently, $\sigma\subsetneqq\tau$). $R$ is a total relation on $\Sigma$, so by $\mathsf{DC}$ there is a sequence $\langle\sigma_n:n\in\Bbb N\rangle$ in $\Sigma$ such that $\sigma_n\mathrel{R}\sigma_{n+1}$ for each $n\in\Bbb N$. Then $\bigcup_{n\in\Bbb N}\sigma_n$ is an infinite sequence $\langle x_k:k\in\Bbb N\rangle$ in $X$ such that $$x_k\notin\bigcup_{\ell<k}B_\epsilon(x_\ell)$$ for each $k\in\Bbb N$.
In fact it’s only when you need to make infinitely many arbitrary choices, recursively or otherwise, that you need any part of the axiom of choice: you can always make any finite number of arbitrary choices.
A: I thought it a bit more through myself, and I guess it is in fact not that hard: Pick a choice function $f$ on (say) $\mathscr P(X)\setminus\{\varnothing\}$, where $\mathscr P(X)$ is the power set of $X$ (another option is a choice function on the set of all non-empty closed subsets of $X$). Then define the sequence $(x_n)$ recursively by
$$
x_{n+1} = f\Big(X\setminus\bigcup_{i=1}^n B_\varepsilon(x_i)\Big).
$$
That gives us the desired sequence.
In other words: Once we have the choice function, we can write down an explicit, recursive construction of $(x_n)$ without further use of the Axiom of Choice.
A: It might be worth adding that you really need the axiom of choice here (to a certain degree anyway).
In Cohen's first model of the axiom of choice there is an infinite Dedekind-finite subset of $\Bbb R$ which is dense. Namely, there is a set $D\subseteq\Bbb R$ which is infinite, but has no countably infinite subsets.
By this virtue alone it is clear why $D$ (with the induced metric) is sequentially compact, every sequence has only finitely many points, so at least one is repeated infinitely often. So every sequence has a convergent subsequence.
On the other hand, $D$ is dense in $\Bbb R$, so as a metric space the metric is unbounded, it certainly cannot have a finite $\varepsilon$-net for any choice of $\varepsilon$.
