Metamath Proof Explorer

Theorem sstotbnd

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis sstotbnd.2 ⊢ 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
Assertion sstotbnd ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )

Proof

Step Hyp Ref Expression
1 sstotbnd.2 ⊢ 𝑁 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
2 1 sstotbnd2 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
3 elfpw ⊢ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( 𝑢 ⊆ 𝑋 ∧ 𝑢 ∈ Fin ) )
4 3 simprbi ⊢ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑢 ∈ Fin )
5 mptfi ⊢ ( 𝑢 ∈ Fin → ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin )
6 rnfi ⊢ ( ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin → ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin )
7 4 5 6 3syl ⊢ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) → ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin )
8 7 ad2antrl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin )
9 simprr ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
10 eqid ⊢ ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) = ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
11 10 rnmpt ⊢ ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) = { 𝑏 ∣ ∃ 𝑥 ∈ 𝑢 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) }
12 3 simplbi ⊢ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑢 ⊆ 𝑋 )
13 ssrexv ⊢ ( 𝑢 ⊆ 𝑋 → ( ∃ 𝑥 ∈ 𝑢 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
14 12 13 syl ⊢ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( ∃ 𝑥 ∈ 𝑢 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
15 14 ad2antrl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ( ∃ 𝑥 ∈ 𝑢 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
16 15 ss2abdv ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → { 𝑏 ∣ ∃ 𝑥 ∈ 𝑢 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } )
17 11 16 eqsstrid ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } )
18 unieq ⊢ ( 𝑣 = ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∪ 𝑣 = ∪ ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
19 ovex ⊢ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∈ V
20 19 dfiun3 ⊢ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
21 18 20 eqtr4di ⊢ ( 𝑣 = ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∪ 𝑣 = ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
22 21 sseq2d ⊢ ( 𝑣 = ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( 𝑌 ⊆ ∪ 𝑣 ↔ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
23 ssabral ⊢ ( 𝑣 ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ↔ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
24 sseq1 ⊢ ( 𝑣 = ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( 𝑣 ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ↔ ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ) )
25 23 24 bitr3id ⊢ ( 𝑣 = ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ) )
26 22 25 anbi12d ⊢ ( 𝑣 = ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ( ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ↔ ( 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ) ) )
27 26 rspcev ⊢ ( ( ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ∧ ran ( 𝑥 ∈ 𝑢 ↦ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ⊆ { 𝑏 ∣ ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) } ) ) → ∃ 𝑣 ∈ Fin ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
28 8 9 17 27 syl12anc ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ∃ 𝑣 ∈ Fin ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
29 28 rexlimdvaa ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) → ∃ 𝑣 ∈ Fin ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
30 oveq1 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑏 ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
31 30 eqeq2d ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑏 ) → ( 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
32 31 ac6sfi ⊢ ( ( 𝑣 ∈ Fin ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑓 ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
33 32 adantrl ⊢ ( ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
34 33 adantl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
35 frn ⊢ ( 𝑓 : 𝑣 ⟶ 𝑋 → ran 𝑓 ⊆ 𝑋 )
36 35 ad2antrl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ran 𝑓 ⊆ 𝑋 )
37 simplrl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑣 ∈ Fin )
38 ffn ⊢ ( 𝑓 : 𝑣 ⟶ 𝑋 → 𝑓 Fn 𝑣 )
39 38 ad2antrl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑓 Fn 𝑣 )
40 dffn4 ⊢ ( 𝑓 Fn 𝑣 ↔ 𝑓 : 𝑣 –onto→ ran 𝑓 )
41 39 40 sylib ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑓 : 𝑣 –onto→ ran 𝑓 )
42 fofi ⊢ ( ( 𝑣 ∈ Fin ∧ 𝑓 : 𝑣 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
43 37 41 42 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ran 𝑓 ∈ Fin )
44 elfpw ⊢ ( ran 𝑓 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( ran 𝑓 ⊆ 𝑋 ∧ ran 𝑓 ∈ Fin ) )
45 36 43 44 sylanbrc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ran 𝑓 ∈ ( 𝒫 𝑋 ∩ Fin ) )
46 simprrl ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → 𝑌 ⊆ ∪ 𝑣 )
47 46 adantr ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑌 ⊆ ∪ 𝑣 )
48 uniiun ⊢ ∪ 𝑣 = ∪ 𝑏 ∈ 𝑣 𝑏
49 iuneq2 ⊢ ( ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) → ∪ 𝑏 ∈ 𝑣 𝑏 = ∪ 𝑏 ∈ 𝑣 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
50 48 49 eqtrid ⊢ ( ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) → ∪ 𝑣 = ∪ 𝑏 ∈ 𝑣 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
51 50 ad2antll ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ∪ 𝑣 = ∪ 𝑏 ∈ 𝑣 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
52 47 51 sseqtrd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑌 ⊆ ∪ 𝑏 ∈ 𝑣 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
53 30 eleq2d ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑏 ) → ( 𝑦 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑦 ∈ ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
54 53 rexrn ⊢ ( 𝑓 Fn 𝑣 → ( ∃ 𝑥 ∈ ran 𝑓 𝑦 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑏 ∈ 𝑣 𝑦 ∈ ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
55 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑥 ∈ ran 𝑓 𝑦 ∈ ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
56 eliun ⊢ ( 𝑦 ∈ ∪ 𝑏 ∈ 𝑣 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑏 ∈ 𝑣 𝑦 ∈ ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
57 54 55 56 3bitr4g ⊢ ( 𝑓 Fn 𝑣 → ( 𝑦 ∈ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑦 ∈ ∪ 𝑏 ∈ 𝑣 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) )
58 57 eqrdv ⊢ ( 𝑓 Fn 𝑣 → ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ 𝑏 ∈ 𝑣 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
59 39 58 syl ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ 𝑏 ∈ 𝑣 ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) )
60 52 59 sseqtrrd ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → 𝑌 ⊆ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
61 iuneq1 ⊢ ( 𝑢 = ran 𝑓 → ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) = ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
62 61 sseq2d ⊢ ( 𝑢 = ran 𝑓 → ( 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ 𝑌 ⊆ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
63 62 rspcev ⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑌 ⊆ ∪ 𝑥 ∈ ran 𝑓 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
64 45 60 63 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) ∧ ( 𝑓 : 𝑣 ⟶ 𝑋 ∧ ∀ 𝑏 ∈ 𝑣 𝑏 = ( ( 𝑓 ‘ 𝑏 ) ( ball ‘ 𝑀 ) 𝑑 ) ) ) → ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
65 34 64 exlimddv ⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ Fin ∧ ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) ) → ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) )
66 65 rexlimdvaa ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ∃ 𝑣 ∈ Fin ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) → ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) )
67 29 66 impbid ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∃ 𝑣 ∈ Fin ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
68 67 ralbidv ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑢 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 ⊆ ∪ 𝑥 ∈ 𝑢 ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )
69 2 68 bitrd ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑁 ∈ ( TotBnd ‘ 𝑌 ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑣 ∈ Fin ( 𝑌 ⊆ ∪ 𝑣 ∧ ∀ 𝑏 ∈ 𝑣 ∃ 𝑥 ∈ 𝑋 𝑏 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑑 ) ) ) )