This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑋 = ∅ → ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ 𝑀 ∈ ( Met ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑋 = ∅ → ( TotBnd ‘ 𝑋 ) = ( TotBnd ‘ ∅ ) )
2 1 eleq2d ⊢ ( 𝑋 = ∅ → ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ 𝑀 ∈ ( TotBnd ‘ ∅ ) ) )
3 0elpw ⊢ ∅ ∈ 𝒫 ∅
4 0fi ⊢ ∅ ∈ Fin
5 elin ⊢ ( ∅ ∈ ( 𝒫 ∅ ∩ Fin ) ↔ ( ∅ ∈ 𝒫 ∅ ∧ ∅ ∈ Fin ) )
6 3 4 5 mpbir2an ⊢ ∅ ∈ ( 𝒫 ∅ ∩ Fin )
7 0iun ⊢ ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅
8 iuneq1 ⊢ ( 𝑣 = ∅ → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
9 8 eqeq1d ⊢ ( 𝑣 = ∅ → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ ↔ ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ ) )
10 9 rspcev ⊢ ( ( ∅ ∈ ( 𝒫 ∅ ∩ Fin ) ∧ ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ ) → ∃ 𝑣 ∈ ( 𝒫 ∅ ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ )
11 6 7 10 mp2an ⊢ ∃ 𝑣 ∈ ( 𝒫 ∅ ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅
12 11 rgenw ⊢ ∀ 𝑟 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 ∅ ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅
13 istotbnd3 ⊢ ( 𝑀 ∈ ( TotBnd ‘ ∅ ) ↔ ( 𝑀 ∈ ( Met ‘ ∅ ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 ∅ ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ ) )
14 12 13 mpbiran2 ⊢ ( 𝑀 ∈ ( TotBnd ‘ ∅ ) ↔ 𝑀 ∈ ( Met ‘ ∅ ) )
15 fveq2 ⊢ ( 𝑋 = ∅ → ( Met ‘ 𝑋 ) = ( Met ‘ ∅ ) )
16 15 eleq2d ⊢ ( 𝑋 = ∅ → ( 𝑀 ∈ ( Met ‘ 𝑋 ) ↔ 𝑀 ∈ ( Met ‘ ∅ ) ) )
17 14 16 bitr4id ⊢ ( 𝑋 = ∅ → ( 𝑀 ∈ ( TotBnd ‘ ∅ ) ↔ 𝑀 ∈ ( Met ‘ 𝑋 ) ) )
18 2 17 bitrd ⊢ ( 𝑋 = ∅ → ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ 𝑀 ∈ ( Met ‘ 𝑋 ) ) )