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 ‘ 𝑋 ) ) )