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=∅→M∈TotBnd⁡X↔M∈Met⁡X

Proof

Step Hyp Ref Expression
1 fveq2 ⊢X=∅→TotBnd⁡X=TotBnd⁡∅
2 1 eleq2d ⊢X=∅→M∈TotBnd⁡X↔M∈TotBnd⁡∅
3 0elpw ⊢∅∈𝒫∅
4 0fin ⊢∅∈Fin
5 elin ⊢∅∈𝒫∅∩Fin↔∅∈𝒫∅∧∅∈Fin
6 3 4 5 mpbir2an ⊢∅∈𝒫∅∩Fin
7 0iun ⊢⋃x∈∅xball⁡Mr=∅
8 iuneq1 ⊢v=∅→⋃x∈vxball⁡Mr=⋃x∈∅xball⁡Mr
9 8 eqeq1d ⊢v=∅→⋃x∈vxball⁡Mr=∅↔⋃x∈∅xball⁡Mr=∅
10 9 rspcev ⊢∅∈𝒫∅∩Fin∧⋃x∈∅xball⁡Mr=∅→∃v∈𝒫∅∩Fin⋃x∈vxball⁡Mr=∅
11 6 7 10 mp2an ⊢∃v∈𝒫∅∩Fin⋃x∈vxball⁡Mr=∅
12 11 rgenw ⊢∀r∈ℝ+∃v∈𝒫∅∩Fin⋃x∈vxball⁡Mr=∅
13 istotbnd3 ⊢M∈TotBnd⁡∅↔M∈Met⁡∅∧∀r∈ℝ+∃v∈𝒫∅∩Fin⋃x∈vxball⁡Mr=∅
14 12 13 mpbiran2 ⊢M∈TotBnd⁡∅↔M∈Met⁡∅
15 fveq2 ⊢X=∅→Met⁡X=Met⁡∅
16 15 eleq2d ⊢X=∅→M∈Met⁡X↔M∈Met⁡∅
17 14 16 bitr4id ⊢X=∅→M∈TotBnd⁡∅↔M∈Met⁡X
18 2 17 bitrd ⊢X=∅→M∈TotBnd⁡X↔M∈Met⁡X