Proof of A Nonempty 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)$. By Compact Subset Criterion via Open Covers in the Ambient Space it suffices to produce a natural number $n$ and elements $i_1,\dots,i_n\in I$ with $K\subseteq U_{i_1}\cup\cdots\cup U_{i_n}$.

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

If $F$ were empty this union would be empty and $K$ would be empty, contrary to hypothesis; so $F$ is nonempty. Being finite and nonempty, $F$ has $n$ elements for some $n\in\mathbb{N}$, by Finite Set; fix such an $n$ together with a bijection $c$ from the initial segment $[n]$ onto $F$, writing $c_m$ for the value of $c$ at $m$.

Step 3 (an index for each net point). By claims 1, 2, and 3 of Properties of the Order on the Natural Numbers, the order on $\mathbb{N}$ is a total order, so the minimum of two natural numbers is defined. For $m\in\mathbb{N}$ put $p_m=\min\{m,n\}$ and

By claim 1 of Elementary Properties of the Minimum of Two Elements we have $p_m\le n$, so $p_m\in[n]$ by Initial Segment of the Natural Numbers and $c_{p_m}$ is defined and lies in $F\subseteq K$. Hence Step 1 applied to the point $c_{p_m}$ shows $A_m$ is nonempty. Each $A_m$ is a subset of $I$, so by Axiom of Countable Choice, applied to the family of subsets of $I$ $(A_m)_{m\in\mathbb{N}}$, there is a sequence $(i_m)_{m\in\mathbb{N}}$ in $I$ with $i_m\in A_m$ for every $m\in\mathbb{N}$.

Step 4 (the finite subcover). Let $m\in[n]$, so $m\le n$ and therefore $p_m=\min\{m,n\}=m$ by Minimum of Two Elements of a Totally Ordered Set. Since $i_m\in A_m$, this gives

Because $c$ maps $[n]$ onto $F$, every $a\in F$ equals $c_m$ for some $m\in[n]$, so

Combining with Step 2 yields $K\subseteq U_{i_1}\cup\cdots\cup U_{i_n}$.

Since the open cover was arbitrary, Compact Subset Criterion via Open Covers in the Ambient Space shows that $K$ is compact in $(X,\mathcal{T}_d)$.