Let Ξ΅ be a real number with Ξ΅>0, and suppose for contradiction that no finite subset FβK satisfies KββaβFβBdβ(a,Ξ΅).
Step 1 (a relation to iterate). Let S be the set of all finite subsets of K. The empty set is finite and is a subset of K, so β
βS and S is nonempty. Define a binary relation R on S, that is a subset of the Cartesian product SΓS, by declaring (F,G)βR exactly when there is yβK with
yβ/aβFββBdβ(a,Ξ΅)andG=Fβͺ{y}.
We check that for every FβS there is GβS with (F,G)βR. Let FβS. By the contradiction hypothesis KββaβFβBdβ(a,Ξ΅) fails, so there is yβK with yβ/βaβFβBdβ(a,Ξ΅). For each aβF the identity-of-indiscernibles axiom of a metric gives d(a,a)=0<Ξ΅, so aβBdβ(a,Ξ΅) by Open Ball in a Metric Space; since y lies in none of these balls, yξ =a. Hence yβ/F, and by claim 2 of Basic Properties of Finite Sets the set Fβͺ{y} is finite: if F is empty it equals {y}, which has 1 element, and if F has k elements it has Ο(k) elements, where Ο denotes the successor map of Natural Numbers. It is also a subset of K. So G=Fβͺ{y} lies in S and (F,G)βR.
Step 2 (an infinite Ξ΅-separated sequence). By Axiom of Dependent Choice, applied to S, R, and the starting element β
, there is a sequence (Fmβ)mβNβ in S with F1β=β
and (Fmβ,Fm+1β)βR for every mβN.
Fix mβN. Any y witnessing (Fmβ,Fm+1β)βR satisfies yβ/Fmβ, by the argument of Step 1, and Fm+1β=Fmββͺ{y}, so Fm+1ββFmβ={y}. Hence Fm+1ββFmβ has exactly one element, and that element is a witness; define xmβ to be it. No choice principle is involved, since xmβ is determined by Fmβ and Fm+1β. Thus (xmβ)mβNβ is a sequence in X with xmββK, and for every m,
FmββFm+1β,xmββFm+1β,xmββ/aβFmβββBdβ(a,Ξ΅).
An induction using the principle of induction and the first of these gives FjββFmβ whenever jβ€m.
Now let j,mβN with j<m. By claim 7 of Properties of the Order on the Natural Numbers there is tβN with m=j+t, and 1β€t by claim 4, so j+1β€j+t=m by claim 6. Hence Fj+1ββFmβ and therefore xjββFmβ. Since xmββ/βaβFmββBdβ(a,Ξ΅), in particular xmββ/Bdβ(xjβ,Ξ΅), so d(xjβ,xmβ)<Ξ΅ fails and comparability of the order on R gives
Ξ΅β€d(xjβ,xmβ).
Step 3 (contradiction with sequential compactness). By Sequentially Compact Subset of a Metric Space there are xβK and a strictly increasing sequence (nkβ)kβNβ in N, in the sense of Subsequence of a Sequence in a Set, such that (xnkββ)kβNβ converges to x in (X,d). By claim 8 of Elementary Order Arithmetic in an Ordered Field, 0<Ξ΅β
2β1 and Ξ΅β
2β1+Ξ΅β
2β1=Ξ΅.
By Convergent Sequence in a Metric Space there is NβN with d(xnkββ,x)<Ξ΅β
2β1 for every k with Nβ€k. Both k=N and k=N+1 satisfy Nβ€k, by claims 1 and 6 of Properties of the Order on the Natural Numbers. Since (nkβ) is strictly increasing, nNβ<nN+1β, so Step 2 gives Ξ΅β€d(xnNββ,xnN+1ββ).
On the other hand, the symmetry axiom of a metric gives d(x,xnN+1ββ)=d(xnN+1ββ,x), so adding the two strict inequalities by claim 3 of Elementary Order Arithmetic in an Ordered Field,
d(xnNββ,x)+d(x,xnN+1ββ)<Ξ΅β
2β1+Ξ΅β
2β1=Ξ΅,
and the triangle inequality axiom gives d(xnNββ,xnN+1ββ)β€d(xnNββ,x)+d(x,xnN+1ββ). By claim 2 of Elementary Order Arithmetic in an Ordered Field we conclude d(xnNββ,xnN+1ββ)<Ξ΅, and combining with Ξ΅β€d(xnNββ,xnN+1ββ) gives Ξ΅<Ξ΅, which is false.
This contradiction shows that some finite subset FβK satisfies KββaβFβBdβ(a,Ξ΅). Since such an F is also a finite subset of X, and Ξ΅>0 was arbitrary, Totally Bounded Subset of a Metric Space shows that K is totally bounded in (X,d).