# Metamath Proof Explorer

## Theorem 0totbnd

Description: The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion 0totbnd ${⊢}{X}=\varnothing \to \left({M}\in \mathrm{TotBnd}\left({X}\right)↔{M}\in \mathrm{Met}\left({X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{X}=\varnothing \to \mathrm{TotBnd}\left({X}\right)=\mathrm{TotBnd}\left(\varnothing \right)$
2 1 eleq2d ${⊢}{X}=\varnothing \to \left({M}\in \mathrm{TotBnd}\left({X}\right)↔{M}\in \mathrm{TotBnd}\left(\varnothing \right)\right)$
3 fveq2 ${⊢}{X}=\varnothing \to \mathrm{Met}\left({X}\right)=\mathrm{Met}\left(\varnothing \right)$
4 3 eleq2d ${⊢}{X}=\varnothing \to \left({M}\in \mathrm{Met}\left({X}\right)↔{M}\in \mathrm{Met}\left(\varnothing \right)\right)$
5 0elpw ${⊢}\varnothing \in 𝒫\varnothing$
6 0fin ${⊢}\varnothing \in \mathrm{Fin}$
7 elin ${⊢}\varnothing \in \left(𝒫\varnothing \cap \mathrm{Fin}\right)↔\left(\varnothing \in 𝒫\varnothing \wedge \varnothing \in \mathrm{Fin}\right)$
8 5 6 7 mpbir2an ${⊢}\varnothing \in \left(𝒫\varnothing \cap \mathrm{Fin}\right)$
9 0iun ${⊢}\bigcup _{{x}\in \varnothing }\left({x}\mathrm{ball}\left({M}\right){r}\right)=\varnothing$
10 iuneq1 ${⊢}{v}=\varnothing \to \bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){r}\right)=\bigcup _{{x}\in \varnothing }\left({x}\mathrm{ball}\left({M}\right){r}\right)$
11 10 eqeq1d ${⊢}{v}=\varnothing \to \left(\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){r}\right)=\varnothing ↔\bigcup _{{x}\in \varnothing }\left({x}\mathrm{ball}\left({M}\right){r}\right)=\varnothing \right)$
12 11 rspcev ${⊢}\left(\varnothing \in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\wedge \bigcup _{{x}\in \varnothing }\left({x}\mathrm{ball}\left({M}\right){r}\right)=\varnothing \right)\to \exists {v}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){r}\right)=\varnothing$
13 8 9 12 mp2an ${⊢}\exists {v}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){r}\right)=\varnothing$
14 13 rgenw ${⊢}\forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){r}\right)=\varnothing$
15 istotbnd3 ${⊢}{M}\in \mathrm{TotBnd}\left(\varnothing \right)↔\left({M}\in \mathrm{Met}\left(\varnothing \right)\wedge \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {v}}\left({x}\mathrm{ball}\left({M}\right){r}\right)=\varnothing \right)$
16 14 15 mpbiran2 ${⊢}{M}\in \mathrm{TotBnd}\left(\varnothing \right)↔{M}\in \mathrm{Met}\left(\varnothing \right)$
17 4 16 syl6rbbr ${⊢}{X}=\varnothing \to \left({M}\in \mathrm{TotBnd}\left(\varnothing \right)↔{M}\in \mathrm{Met}\left({X}\right)\right)$
18 2 17 bitrd ${⊢}{X}=\varnothing \to \left({M}\in \mathrm{TotBnd}\left({X}\right)↔{M}\in \mathrm{Met}\left({X}\right)\right)$