Theorem: Sequentially Compact Metric Space is Totally Bounded

Let $M = \struct {A, d}$ be a metric space.
Let $M$ be sequentially compact.
Then $M$ is totally bounded.

Proof:
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
By definition, $M$ is totally bounded only if there exists a finite $\epsilon$-net for $M$.
{{AimForCont}} there exists no finite $\epsilon$-net for $M$.
The aim is to construct an infinite sequence $\sequence {x_n}_{n \ge 1}$ in $A$ that has no convergent subsequence.
For all natural numbers $n \ge 1$, define the set:
:$\SS_n = \set {F \subseteq A: \size F = n: \forall x, y \in F: x \ne y \implies \map d {x, y} \ge \epsilon}$
where $\size F$ denotes the cardinality of $F$.
We use the Principle of Mathematical Induction to prove that $\SS_n$ is non-empty.
It is vacuously true that any singleton $\set x \subseteq A$ is an element of $\SS_1$.
Since $A$ is non-empty by the definition of a metric space, it follows from Existence of Singleton Set that $\SS_1$ is non-empty.
Let $F \in \SS_n$.
By definition, $F$ is finite.
So $F$ is not an $\epsilon$-net for $M$, {{hypothesis}}.
Hence, there exists an $x \in A$ such that:
:$\forall y \in F: \map d {x, y} \ge \epsilon$
Note that, by {{Metric-space-axiom|1}}:
:$x \notin F$
Consider the set:
:$F' := F \cup \set x$.
Then:
:$\size {F'} = n + 1$
and by {{Metric-space-axiom|3}}:
:$F' \in \SS_{n + 1}$
Thus, we have proven that $\SS_n$ is non-empty for all natural numbers $n \ge 1$.
Therefore, using the axiom of countable choice, we can obtain an infinite sequence $\sequence {F_n}_{n \ge 1}$ such that:
:$\forall n \in \N_{\ge 1}: F_n \in \SS_n$
From Countable Union of Countable Sets is Countable, there exists an injection:
:$\ds \phi: \bigcup_{n \mathop \ge 1} F_n \to \N$
We now construct an infinite sequence $\sequence {x_n}_{n \ge 1}$ in $A$.
{{explain|This seems a colloquial sense of PoRD, which needs to be formalised in some way}}
To do this, we use the Principle of Recursive Definition to define the sequence $\sequence {\tuple {x_1, x_2, \ldots, x_n} }_{n \ge 1}$ of ordered $n$-tuples.
Let $x_1 \in F_1$.
Suppose that $x_1, x_2, \ldots, x_n$ have been defined, and let:
:$T_n = \set {x_1, x_2, \ldots, x_n}$
Define:
:$D_n = \set {x \in F_{n + 1}: \forall y \in T_n: \map d {x, y} \ge \dfrac \epsilon 2}$
Using a Proof by Contradiction, we show that $D_n$ is non-empty.
For all $x \in F_{n + 1}$, define:
:$\map {C_n} x = \set {y \in T_n: \map d {x, y} < \dfrac \epsilon 2}$
Let $x, x' \in F_{n + 1}$ be distinct.
Let $y \in \map {C_n} x$.
Then it follows from:
:the definition of $F_{n + 1}$
:{{Metric-space-axiom|2}} and {{Metric-space-axiom|3}}:
that:
:$\map d {x', y} \ge \map d {x, x'} - \map d {x, y} > \dfrac \epsilon 2$
Hence, $y \notin \map {C_n} {x'}$.
That is, the indexed family of sets:
:$\sequence {\map {C_n} x}_{x \in F_{n + 1}}$
is pairwise disjoint.
Suppose that $D_n$ is empty.
That is:
:$\forall x \in F_{n + 1}: \map {C_n} x$ is non-empty
Then, from Cardinality is Additive Function, Finite Union of Sets in Additive Function, and Cardinality of Subset of Finite Set, we have:
:$\ds \size {F_{n + 1} } \le \sum_{x \mathop \in F_{n + 1} } \size {\map {C_n} x} \le \size {T_n} < \size {F_{n + 1} }$
which is a contradiction.
{{explain|"Therefore ..." and explain what assumption was made so as to give rise to this contradiction.}}
From the well-ordering principle, we have that $\struct {\N, \le}$ is a well-ordered set.
Let $\le_{\phi}$ be the ordering induced by $\phi$.
Then $\le_{\phi}$ is a well-ordering.
We define $x_{n + 1}$ as the (unique) $\le_{\phi}$-smallest element of $D_n$.
By construction:
:$\forall m, n \in \N_{>0}: m \le n \implies \map d {x_{n + 1}, x_m} \ge \dfrac \epsilon 2$
Hence, by induction, it follows from {{Metric-space-axiom|3}} that:
:$\forall m, n \in \N_{>0}: m \ne n \implies \map d {x_m, x_n} \ge \dfrac \epsilon 2$
Therefore, the sequence $\sequence {x_n}$ has no Cauchy subsequence.
From Convergent Sequence in Metric Space is Cauchy Sequence, $\sequence {x_n}$ has no convergent subsequence either.
Thus, by definition, $M$ is not sequentially compact.
But this contradicts the original assumption that $M$ is sequentially compact.
Thus the assumption that there exists no finite $\epsilon$-net for $M$ was false.
Therefore, by definition, $M$ is totally bounded.
Hence the result.
{{qed}}