A complete, totally bounded metric space is compact, proved from countable choice used exactly once

Suppose $(X,d)$ is complete and totally bounded and that some family $\mathcal{U}$ of open subsets of $X$ with union $X$ has no finite subfamily with union $X$; call a subset $S\subseteq X$ finitely covered when some finite subfamily of $\mathcal{U}$ has union containing $S$, so that $X$ itself is not finitely covered.

$X\mathrm{\ne }\mathrm{\varnothing }$, since the empty subfamily of $\mathcal{U}$ has union $\mathrm{\varnothing }$ and would finitely cover an empty $X$; consequently, for each $n\in \mathbb{N}$, the set $E_n$ of pairs $(m,f)$ with $m\in \mathbb{N}$ and $f:\sigma (m)\to X$ such that $\{f(0),\dots ,f(m)\}$ is a finite $1\mathrm{/}(n+1)$-net for $X$ is nonempty.

Countable choice applied to $(E_n{)}_{n\in \mathbb{N}}$ fixes, once and for all, a function $n\mapsto (m_n,f_n)$ with $(m_n,f_n)\in E_n$; this is the single appeal to a choice principle in this proof, and the family $(E_n)$ was written down at step 2.1 before any of it was made.

If $S\subseteq X$ is not finitely covered and $n\in \mathbb{N}$, then $S\cap B(f_n(i),1\mathrm{/}(n+1))$ fails to be finitely covered for at least one $i\le m_n$: otherwise finite choice applied to $i\mapsto \{\text{finite subfamilies of }\mathcal{U}\text{ covering }S\cap B(f_n(i),1\mathrm{/}(n+1))\}$ produces one such subfamily for each $i\le m_n$, and the concatenation of those finitely many finite lists is a finite subfamily of $\mathcal{U}$ whose union contains $S={\bigcup }_{i\le m_n}(S\cap B(f_n(i),1\mathrm{/}(n+1)))$.

Let $i(n,S)$ be the least $i\le m_n$ with $S\cap B(f_n(i),1\mathrm{/}(n+1))$ not finitely covered when such an $i$ exists, and $0$ otherwise; recursion on $\mathbb{N}\times \mathcal{P}(X)$ with starting value $(0,X)$ and rule $F(n,S):=(n+1,S\cap B(f_n(i(n,S)),1\mathrm{/}(n+1)))$ then produces $g:\mathbb{N}\to \mathbb{N}\times \mathcal{P}(X)$ whose first coordinate at $n$ is $n$; write $A_n$ for its second coordinate and $c_n:=f_n(i(n,A_n))$.

By induction, no $A_n$ is finitely covered: $A_0=X$ is not, by step 1.1, and if $A_n$ is not then step 4.1 supplies an admissible $i$, so $i(n,A_n)$ is one and $A_{n+1}=A_n\cap B(c_n,1\mathrm{/}(n+1))$ is not finitely covered either. In particular every $A_n$ is nonempty, since the empty set is finitely covered by the empty subfamily; moreover $A_{n+1}\subseteq A_n$ and $A_{n+1}\subseteq B(c_n,1\mathrm{/}(n+1))$.

The sequence $(c_n)$ is Cauchy: for $m\ge n$ one has $A_{m+1}\subseteq A_{n+1}\subseteq B(c_n,1\mathrm{/}(n+1))$ and $A_{m+1}\subseteq B(c_m,1\mathrm{/}(m+1))$, and taking $z\in A_{m+1}$ gives $d(c_n,c_m)\le d(c_n,z)+d(z,c_m)<1\mathrm{/}(n+1)+1\mathrm{/}(m+1)\le 2\mathrm{/}(n+1)$; so given a rational $\eta >0$, a natural $N\ge 1$ with $1\mathrm{/}N<\eta \mathrm{/}2$ makes $d(c_n,c_m)<\eta$ for all $n,m\ge N$.

By completeness $c_n\to p$ for some $p\in X$; since $\mathcal{U}$ has union $X$ there is $U\in \mathcal{U}$ with $p\in U$, and openness of $U$ gives a real $r>0$ with $B(p,r)\subseteq U$.

Take a natural $N\ge 1$ with $1\mathrm{/}N<r\mathrm{/}2$, then $K\in \mathbb{N}$ with $d(c_n,p)<1\mathrm{/}N$ for all $n\ge K$, and let $n$ be whichever of $N$ and $K$ is the greater; then $1\mathrm{/}(n+1)<1\mathrm{/}N<r\mathrm{/}2$ and $d(c_n,p)<r\mathrm{/}2$, so every $y\in A_{n+1}\subseteq B(c_n,1\mathrm{/}(n+1))$ satisfies $d(y,p)\le d(y,c_n)+d(c_n,p)<r$, that is $A_{n+1}\subseteq B(p,r)\subseteq U$.

So the one-member subfamily $\{U\}$ of $\mathcal{U}$ has union containing $A_{n+1}$, making $A_{n+1}$ finitely covered and contradicting step 6.1; the assumption of step 1.1 therefore fails, every family of open sets with union $X$ has a finite subfamily with union $X$, and $(X,d)$ is compact.