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 fveq2 ⊢ X = ∅ → Met ⁡ X = Met ⁡ ∅
4 3 eleq2d ⊢ X = ∅ → M ∈ Met ⁡ X ↔ M ∈ Met ⁡ ∅
5 0elpw ⊢ ∅ ∈ 𝒫 ∅
6 0fin ⊢ ∅ ∈ Fin
7 elin ⊢ ∅ ∈ 𝒫 ∅ ∩ Fin ↔ ∅ ∈ 𝒫 ∅ ∧ ∅ ∈ Fin
8 5 6 7 mpbir2an ⊢ ∅ ∈ 𝒫 ∅ ∩ Fin
9 0iun ⊢ ⋃ x ∈ ∅ x ball ⁡ M r = ∅
10 iuneq1 ⊢ v = ∅ → ⋃ x ∈ v x ball ⁡ M r = ⋃ x ∈ ∅ x ball ⁡ M r
11 10 eqeq1d ⊢ v = ∅ → ⋃ x ∈ v x ball ⁡ M r = ∅ ↔ ⋃ x ∈ ∅ x ball ⁡ M r = ∅
12 11 rspcev ⊢ ∅ ∈ 𝒫 ∅ ∩ Fin ∧ ⋃ x ∈ ∅ x ball ⁡ M r = ∅ → ∃ v ∈ 𝒫 ∅ ∩ Fin ⋃ x ∈ v x ball ⁡ M r = ∅
13 8 9 12 mp2an ⊢ ∃ v ∈ 𝒫 ∅ ∩ Fin ⋃ x ∈ v x ball ⁡ M r = ∅
14 13 rgenw ⊢ ∀ r ∈ ℝ + ∃ v ∈ 𝒫 ∅ ∩ Fin ⋃ x ∈ v x ball ⁡ M r = ∅
15 istotbnd3 ⊢ M ∈ TotBnd ⁡ ∅ ↔ M ∈ Met ⁡ ∅ ∧ ∀ r ∈ ℝ + ∃ v ∈ 𝒫 ∅ ∩ Fin ⋃ x ∈ v x ball ⁡ M r = ∅
16 14 15 mpbiran2 ⊢ M ∈ TotBnd ⁡ ∅ ↔ M ∈ Met ⁡ ∅
17 4 16 syl6rbbr ⊢ X = ∅ → M ∈ TotBnd ⁡ ∅ ↔ M ∈ Met ⁡ X
18 2 17 bitrd ⊢ X = ∅ → M ∈ TotBnd ⁡ X ↔ M ∈ Met ⁡ X