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		fveq2	⊢ ( 𝑋 = ∅ → ( Met ‘ 𝑋 ) = ( Met ‘ ∅ ) )
4	3	eleq2d	⊢ ( 𝑋 = ∅ → ( 𝑀 ∈ ( Met ‘ 𝑋 ) ↔ 𝑀 ∈ ( Met ‘ ∅ ) ) )
5		0elpw	⊢ ∅ ∈ 𝒫 ∅
6		0fin	⊢ ∅ ∈ Fin
7		elin	⊢ ( ∅ ∈ ( 𝒫 ∅ ∩ Fin ) ↔ ( ∅ ∈ 𝒫 ∅ ∧ ∅ ∈ Fin ) )
8	5 6 7	mpbir2an	⊢ ∅ ∈ ( 𝒫 ∅ ∩ Fin )
9		0iun	⊢ ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅
10		iuneq1	⊢ ( 𝑣 = ∅ → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
11	10	eqeq1d	⊢ ( 𝑣 = ∅ → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ ↔ ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ ) )
12	11	rspcev	⊢ ( ( ∅ ∈ ( 𝒫 ∅ ∩ Fin ) ∧ ∪ 𝑥 ∈ ∅ ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ ) → ∃ 𝑣 ∈ ( 𝒫 ∅ ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ )
13	8 9 12	mp2an	⊢ ∃ 𝑣 ∈ ( 𝒫 ∅ ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅
14	13	rgenw	⊢ ∀ 𝑟 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 ∅ ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅
15		istotbnd3	⊢ ( 𝑀 ∈ ( TotBnd ‘ ∅ ) ↔ ( 𝑀 ∈ ( Met ‘ ∅ ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 ∅ ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ∅ ) )
16	14 15	mpbiran2	⊢ ( 𝑀 ∈ ( TotBnd ‘ ∅ ) ↔ 𝑀 ∈ ( Met ‘ ∅ ) )
17	4 16	syl6rbbr	⊢ ( 𝑋 = ∅ → ( 𝑀 ∈ ( TotBnd ‘ ∅ ) ↔ 𝑀 ∈ ( Met ‘ 𝑋 ) ) )
18	2 17	bitrd	⊢ ( 𝑋 = ∅ → ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ 𝑀 ∈ ( Met ‘ 𝑋 ) ) )