Metamath Proof Explorer

Theorem istotbnd3

Description: A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion istotbnd3 ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 istotbnd ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
2 oveq1 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑏 ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
3 2 eqeq2d ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑏 ) → ( 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
4 3 ac6sfi ⊢ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
5 4 ex ⊢ ( 𝑤 ∈ Fin → ( ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
6 5 ad2antlr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ∪ 𝑤 = 𝑋 ) → ( ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
7 simprrl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → 𝑓 : 𝑤 ⟶ 𝑋 )
8 7 frnd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ran 𝑓 ⊆ 𝑋 )
9 simplr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → 𝑤 ∈ Fin )
10 7 ffnd ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → 𝑓 Fn 𝑤 )
11 dffn4 ⊢ ( 𝑓 Fn 𝑤 ↔ 𝑓 : 𝑤 –onto→ ran 𝑓 )
12 10 11 sylib ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → 𝑓 : 𝑤 –onto→ ran 𝑓 )
13 fofi ⊢ ( ( 𝑤 ∈ Fin ∧ 𝑓 : 𝑤 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
14 9 12 13 syl2anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ran 𝑓 ∈ Fin )
15 elfpw ⊢ ( ran 𝑓 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( ran 𝑓 ⊆ 𝑋 ∧ ran 𝑓 ∈ Fin ) )
16 8 14 15 sylanbrc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ran 𝑓 ∈ ( 𝒫 𝑋 ∩ Fin ) )
17 2 eleq2d ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑏 ) → ( 𝑣 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑣 ∈ ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
18 17 rexrn ⊢ ( 𝑓 Fn 𝑤 → ( ∃ 𝑥 ∈ ran 𝑓 𝑣 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑏 ∈ 𝑤 𝑣 ∈ ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
19 10 18 syl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ( ∃ 𝑥 ∈ ran 𝑓 𝑣 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑏 ∈ 𝑤 𝑣 ∈ ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
20 eliun ⊢ ( 𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑥 ∈ ran 𝑓 𝑣 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
21 eliun ⊢ ( 𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑏 ∈ 𝑤 𝑣 ∈ ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
22 19 20 21 3bitr4g ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ( 𝑣 ∈ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑣 ∈ ∪ 𝑏 ∈ 𝑤 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
23 22 eqrdv ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ 𝑏 ∈ 𝑤 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
24 simprrr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
25 iuneq2 ⊢ ( ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
26 24 25 syl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∪ 𝑏 ∈ 𝑤 𝑏 = ∪ 𝑏 ∈ 𝑤 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
27 uniiun ⊢ ∪ 𝑤 = ∪ 𝑏 ∈ 𝑤 𝑏
28 simprl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∪ 𝑤 = 𝑋 )
29 27 28 eqtr3id ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∪ 𝑏 ∈ 𝑤 𝑏 = 𝑋 )
30 23 26 29 3eqtr2d ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 )
31 iuneq1 ⊢ ( 𝑣 = ran 𝑓 → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
32 31 eqeq1d ⊢ ( 𝑣 = ran 𝑓 → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ↔ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
33 32 rspcev ⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 )
34 16 30 33 syl2anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ( ∪ 𝑤 = 𝑋 ∧ ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 )
35 34 expr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ∪ 𝑤 = 𝑋 ) → ( ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
36 35 exlimdv ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ∪ 𝑤 = 𝑋 ) → ( ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
37 6 36 syld ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) ∧ ∪ 𝑤 = 𝑋 ) → ( ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
38 37 expimpd ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑤 ∈ Fin ) → ( ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
39 38 rexlimdva ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
40 elfpw ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( 𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin ) )
41 40 simprbi ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑣 ∈ Fin )
42 41 ad2antrl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → 𝑣 ∈ Fin )
43 mptfi ⊢ ( 𝑣 ∈ Fin → ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin )
44 rnfi ⊢ ( ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin → ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin )
45 42 43 44 3syl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin )
46 ovex ⊢ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∈ V
47 46 dfiun3 ⊢ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
48 simprr ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 )
49 47 48 eqtr3id ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → ∪ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) = 𝑋 )
50 eqid ⊢ ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) = ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
51 50 rnmpt ⊢ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) = { 𝑏 ∣ ∃ 𝑥 ∈ 𝑣 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) }
52 40 simplbi ⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑣 ⊆ 𝑋 )
53 52 ad2antrl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → 𝑣 ⊆ 𝑋 )
54 ssrexv ⊢ ( 𝑣 ⊆ 𝑋 → ( ∃ 𝑥 ∈ 𝑣 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
55 53 54 syl ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → ( ∃ 𝑥 ∈ 𝑣 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
56 55 ss2abdv ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → { 𝑏 ∣ ∃ 𝑥 ∈ 𝑣 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } )
57 51 56 eqsstrid ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } )
58 unieq ⊢ ( 𝑤 = ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∪ 𝑤 = ∪ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
59 58 eqeq1d ⊢ ( 𝑤 = ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( ∪ 𝑤 = 𝑋 ↔ ∪ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) = 𝑋 ) )
60 ssabral ⊢ ( 𝑤 ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ↔ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
61 sseq1 ⊢ ( 𝑤 = ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( 𝑤 ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ↔ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ) )
62 60 61 bitr3id ⊢ ( 𝑤 = ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ) )
63 59 62 anbi12d ⊢ ( 𝑤 = ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ↔ ( ∪ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) = 𝑋 ∧ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ) ) )
64 63 rspcev ⊢ ( ( ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin ∧ ( ∪ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) = 𝑋 ∧ ran ( 𝑥 ∈ 𝑣 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ) ) → ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
65 45 49 57 64 syl12anc ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) ) → ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
66 65 expr ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 → ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
67 66 rexlimdva ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 → ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
68 39 67 impbid ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ↔ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
69 68 ralbidv ⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
70 69 pm5.32i ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑤 ∈ Fin ( ∪ 𝑤 = 𝑋 ∧ ∀ 𝑏 ∈ 𝑤 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )
71 1 70 bitri ⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = 𝑋 ) )