Proof of A Sequentially Compact Subset of a Metric Space is Compact

Let $I$ be a set and let $(U_i)_{i\in I}$ be an open cover of $K$ in $(X,\mathcal{T}_d)$. We produce a finite subset $J\subseteq I$ with $K\subseteq\bigcup_{j\in J}U_j$. Since the cover is arbitrary, this establishes statement 2 of Compact Subset Criterion via Open Covers in the Ambient Space for $K$, hence statement 1 of that theorem, namely that $K$ is compact in $(X,\mathcal{T}_d)$.

Step 1 (a Lebesgue number). By Lebesgue Number Lemma for a Sequentially Compact Subset of a Metric Space there is a real number $\delta>0$ such that for every $x\in K$ there is $i\in I$ with $B_d(x,\delta)\subseteq U_i$, where $B_d(x,\delta)$ is the open ball in $X$ with center $x$ and radius $\delta$.

Step 2 (a finite net inside $K$). By A Sequentially Compact Subset of a Metric Space is Totally Bounded applied with $\varepsilon=\delta$, there is a finite subset $F\subseteq K$ with

$$K\subseteq\bigcup_{a\in F}B_d(a,\delta),$$

where a union indexed by the empty set is empty.

Step 3 (an index for each net point). For $a\in F$ put

$$A_a=\{i\in I:\ B_d(a,\delta)\subseteq U_i\},$$

so that $(A_a)_{a\in F}$ is a family of subsets of $I$. Since $a\in F\subseteq K$, Step 1 applied to the point $a$ shows that $A_a$ is nonempty. The index set $F$ is finite, so Choice for a Family Indexed by a Finite Set provides a function $\iota:F\to I$ with $\iota(a)\in A_a$ for every $a\in F$, that is,

$$B_d(a,\delta)\subseteq U_{\iota(a)}\qquad\text{for every }a\in F.$$

Step 4 (the finite subcover). Put $J=\{\iota(a):a\in F\}$, a subset of $I$. If $F=\emptyset$ then $J=\emptyset$, which is finite by Finite Set. Otherwise $F$ is finite and nonempty, so it has $n$ elements for some natural number $n$, and $\iota$ maps $F$ onto $J$ by the definition of $J$; hence $J$ is finite by claim 4 of Basic Properties of Finite Sets. In either case $J$ is a finite subset of $I$.

Finally, let $x\in K$. By Step 2 there is $a\in F$ with $x\in B_d(a,\delta)$, and by Step 3 $B_d(a,\delta)\subseteq U_{\iota(a)}$, so $x\in U_{\iota(a)}$ with $\iota(a)\in J$. Therefore

$$K\subseteq\bigcup_{j\in J}U_j,$$

as required.