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 0fin ∅ ∈ 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 ‘ 𝑋 ) ) )