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 ∈ ∅ x ball ⁡ M r = ∅
8 iuneq1 ⊢ v = ∅ → ⋃ x ∈ v x ball ⁡ M r = ⋃ x ∈ ∅ x ball ⁡ M r
9 8 eqeq1d ⊢ v = ∅ → ⋃ x ∈ v x ball ⁡ M r = ∅ ↔ ⋃ x ∈ ∅ x ball ⁡ M r = ∅
10 9 rspcev ⊢ ∅ ∈ 𝒫 ∅ ∩ Fin ∧ ⋃ x ∈ ∅ x ball ⁡ M r = ∅ → ∃ v ∈ 𝒫 ∅ ∩ Fin ⋃ x ∈ v x ball ⁡ M r = ∅
11 6 7 10 mp2an ⊢ ∃ v ∈ 𝒫 ∅ ∩ Fin ⋃ x ∈ v x ball ⁡ M r = ∅
12 11 rgenw ⊢ ∀ r ∈ ℝ + ∃ v ∈ 𝒫 ∅ ∩ Fin ⋃ x ∈ v x ball ⁡ M r = ∅
13 istotbnd3 ⊢ M ∈ TotBnd ⁡ ∅ ↔ M ∈ Met ⁡ ∅ ∧ ∀ r ∈ ℝ + ∃ v ∈ 𝒫 ∅ ∩ Fin ⋃ x ∈ v x ball ⁡ M r = ∅
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