Metamath Proof Explorer

Theorem heibor

Description: Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 and heiborlem1 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 28-Jan-2014)

Ref Expression
Hypothesis heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion heibor ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 ∈ Comp ) ↔ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 heibor1 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 ∈ Comp ) → ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ) )
3 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
4 3 adantr ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
5 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
6 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
7 3 5 6 3syl ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐽 ∈ Top )
8 7 adantr ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ) → 𝐽 ∈ Top )
9 istotbnd ⊢ ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) ) )
10 9 simprbi ⊢ ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) )
11 2nn ⊢ 2 ∈ ℕ
12 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
13 11 12 mpan ⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℕ )
14 13 nnrpd ⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
15 14 rpreccld ⊢ ( 𝑛 ∈ ℕ0 → ( 1 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ )
16 oveq2 ⊢ ( 𝑟 = ( 1 / ( 2 ↑ 𝑛 ) ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
17 16 eqeq2d ⊢ ( 𝑟 = ( 1 / ( 2 ↑ 𝑛 ) ) → ( 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
18 17 rexbidv ⊢ ( 𝑟 = ( 1 / ( 2 ↑ 𝑛 ) ) → ( ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
19 18 ralbidv ⊢ ( 𝑟 = ( 1 / ( 2 ↑ 𝑛 ) ) → ( ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ↔ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
20 19 anbi2d ⊢ ( 𝑟 = ( 1 / ( 2 ↑ 𝑛 ) ) → ( ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) ↔ ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
21 20 rexbidv ⊢ ( 𝑟 = ( 1 / ( 2 ↑ 𝑛 ) ) → ( ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) ↔ ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
22 21 rspccva ⊢ ( ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ) ∧ ( 1 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ ) → ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
23 10 15 22 syl2an ⊢ ( ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
24 23 expcom ⊢ ( 𝑛 ∈ ℕ0 → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) → ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
25 24 adantl ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) → ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
26 oveq1 ⊢ ( 𝑦 = ( 𝑚 ‘ 𝑣 ) → ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
27 26 eqeq2d ⊢ ( 𝑦 = ( 𝑚 ‘ 𝑣 ) → ( 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
28 27 ac6sfi ⊢ ( ( 𝑢 ∈ Fin ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) → ∃ 𝑚 ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
29 28 adantrl ⊢ ( ( 𝑢 ∈ Fin ∧ ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∃ 𝑚 ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
30 29 adantl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ∃ 𝑚 ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
31 simp3l ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝑚 : 𝑢 ⟶ 𝑋 )
32 31 frnd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ran 𝑚 ⊆ 𝑋 )
33 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
34 3 5 33 3syl ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
35 34 adantr ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑋 = ∪ 𝐽 )
36 35 3ad2ant1 ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝑋 = ∪ 𝐽 )
37 32 36 sseqtrd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ran 𝑚 ⊆ ∪ 𝐽 )
38 1 fvexi ⊢ 𝐽 ∈ V
39 38 uniex ⊢ ∪ 𝐽 ∈ V
40 39 elpw2 ⊢ ( ran 𝑚 ∈ 𝒫 ∪ 𝐽 ↔ ran 𝑚 ⊆ ∪ 𝐽 )
41 37 40 sylibr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ran 𝑚 ∈ 𝒫 ∪ 𝐽 )
42 simp2l ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝑢 ∈ Fin )
43 ffn ⊢ ( 𝑚 : 𝑢 ⟶ 𝑋 → 𝑚 Fn 𝑢 )
44 dffn4 ⊢ ( 𝑚 Fn 𝑢 ↔ 𝑚 : 𝑢 –onto→ ran 𝑚 )
45 43 44 sylib ⊢ ( 𝑚 : 𝑢 ⟶ 𝑋 → 𝑚 : 𝑢 –onto→ ran 𝑚 )
46 fofi ⊢ ( ( 𝑢 ∈ Fin ∧ 𝑚 : 𝑢 –onto→ ran 𝑚 ) → ran 𝑚 ∈ Fin )
47 45 46 sylan2 ⊢ ( ( 𝑢 ∈ Fin ∧ 𝑚 : 𝑢 ⟶ 𝑋 ) → ran 𝑚 ∈ Fin )
48 42 31 47 syl2anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ran 𝑚 ∈ Fin )
49 41 48 elind ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ran 𝑚 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) )
50 26 eleq2d ⊢ ( 𝑦 = ( 𝑚 ‘ 𝑣 ) → ( 𝑟 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ 𝑟 ∈ ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
51 50 rexrn ⊢ ( 𝑚 Fn 𝑢 → ( ∃ 𝑦 ∈ ran 𝑚 𝑟 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ ∃ 𝑣 ∈ 𝑢 𝑟 ∈ ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
52 eliun ⊢ ( 𝑟 ∈ ∪ 𝑦 ∈ ran 𝑚 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ ∃ 𝑦 ∈ ran 𝑚 𝑟 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
53 eliun ⊢ ( 𝑟 ∈ ∪ 𝑣 ∈ 𝑢 ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ ∃ 𝑣 ∈ 𝑢 𝑟 ∈ ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
54 51 52 53 3bitr4g ⊢ ( 𝑚 Fn 𝑢 → ( 𝑟 ∈ ∪ 𝑦 ∈ ran 𝑚 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ 𝑟 ∈ ∪ 𝑣 ∈ 𝑢 ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
55 54 eqrdv ⊢ ( 𝑚 Fn 𝑢 → ∪ 𝑦 ∈ ran 𝑚 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) = ∪ 𝑣 ∈ 𝑢 ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
56 31 43 55 3syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∪ 𝑦 ∈ ran 𝑚 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) = ∪ 𝑣 ∈ 𝑢 ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
57 simp3r ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
58 uniiun ⊢ ∪ 𝑢 = ∪ 𝑣 ∈ 𝑢 𝑣
59 iuneq2 ⊢ ( ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) → ∪ 𝑣 ∈ 𝑢 𝑣 = ∪ 𝑣 ∈ 𝑢 ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
60 58 59 syl5eq ⊢ ( ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) → ∪ 𝑢 = ∪ 𝑣 ∈ 𝑢 ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
61 57 60 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∪ 𝑢 = ∪ 𝑣 ∈ 𝑢 ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
62 simp2r ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∪ 𝑢 = 𝑋 )
63 56 61 62 3eqtr2rd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝑋 = ∪ 𝑦 ∈ ran 𝑚 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
64 iuneq1 ⊢ ( 𝑡 = ran 𝑚 → ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) = ∪ 𝑦 ∈ ran 𝑚 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
65 64 rspceeqv ⊢ ( ( ran 𝑚 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ 𝑋 = ∪ 𝑦 ∈ ran 𝑚 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) → ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
66 49 63 65 syl2anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ∧ ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
67 66 3expia ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ∪ 𝑢 = 𝑋 ) ) → ( ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) → ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
68 67 adantrrr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ( ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) → ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
69 68 exlimdv ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ( ∃ 𝑚 ( 𝑚 : 𝑢 ⟶ 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 𝑣 = ( ( 𝑚 ‘ 𝑣 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) → ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
70 30 69 mpd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑢 ∈ Fin ∧ ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
71 70 rexlimdvaa ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( ∃ 𝑢 ∈ Fin ( ∪ 𝑢 = 𝑋 ∧ ∀ 𝑣 ∈ 𝑢 ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) → ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
72 25 71 syld ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) → ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
73 72 ralrimdva ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) → ∀ 𝑛 ∈ ℕ0 ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
74 39 pwex ⊢ 𝒫 ∪ 𝐽 ∈ V
75 74 inex1 ⊢ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∈ V
76 nn0ennn ⊢ ℕ0 ≈ ℕ
77 nnenom ⊢ ℕ ≈ ω
78 76 77 entri ⊢ ℕ0 ≈ ω
79 iuneq1 ⊢ ( 𝑡 = ( 𝑚 ‘ 𝑛 ) → ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
80 79 eqeq2d ⊢ ( 𝑡 = ( 𝑚 ‘ 𝑛 ) → ( 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
81 75 78 80 axcc4 ⊢ ( ∀ 𝑛 ∈ ℕ0 ∃ 𝑡 ∈ ( 𝒫 ∪ 𝐽 ∩ Fin ) 𝑋 = ∪ 𝑦 ∈ 𝑡 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) → ∃ 𝑚 ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
82 73 81 syl6 ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) → ∃ 𝑚 ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
83 elpwi ⊢ ( 𝑟 ∈ 𝒫 𝐽 → 𝑟 ⊆ 𝐽 )
84 eqid ⊢ { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 } = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
85 eqid ⊢ { ⟨ 𝑡 , 𝑘 ⟩ ∣ ( 𝑘 ∈ ℕ0 ∧ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ∧ ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑘 ) ∈ { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 } ) } = { ⟨ 𝑡 , 𝑘 ⟩ ∣ ( 𝑘 ∈ ℕ0 ∧ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ∧ ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑘 ) ∈ { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 } ) }
86 eqid ⊢ ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
87 simpl ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
88 34 pweqd ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝒫 𝑋 = 𝒫 ∪ 𝐽 )
89 88 ineq1d ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( 𝒫 𝑋 ∩ Fin ) = ( 𝒫 ∪ 𝐽 ∩ Fin ) )
90 89 feq3d ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( 𝑚 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) ↔ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) )
91 90 biimpar ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) → 𝑚 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
92 91 adantrr ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝑚 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
93 oveq1 ⊢ ( 𝑡 = 𝑦 → ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ( 𝑦 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) )
94 93 cbviunv ⊢ ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 )
95 id ⊢ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) → 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) )
96 inss1 ⊢ ( 𝒫 ∪ 𝐽 ∩ Fin ) ⊆ 𝒫 ∪ 𝐽
97 96 88 sseqtrrid ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( 𝒫 ∪ 𝐽 ∩ Fin ) ⊆ 𝒫 𝑋 )
98 fss ⊢ ( ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ( 𝒫 ∪ 𝐽 ∩ Fin ) ⊆ 𝒫 𝑋 ) → 𝑚 : ℕ0 ⟶ 𝒫 𝑋 )
99 95 97 98 syl2anr ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) → 𝑚 : ℕ0 ⟶ 𝒫 𝑋 )
100 99 ffvelrnda ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑚 ‘ 𝑛 ) ∈ 𝒫 𝑋 )
101 100 elpwid ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑚 ‘ 𝑛 ) ⊆ 𝑋 )
102 101 sselda ⊢ ( ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ) → 𝑦 ∈ 𝑋 )
103 simplr ⊢ ( ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ) → 𝑛 ∈ ℕ0 )
104 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
105 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑛 ) )
106 105 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 1 / ( 2 ↑ 𝑚 ) ) = ( 1 / ( 2 ↑ 𝑛 ) ) )
107 106 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
108 ovex ⊢ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ∈ V
109 104 107 86 108 ovmpo ⊢ ( ( 𝑦 ∈ 𝑋 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑦 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
110 102 103 109 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ) → ( 𝑦 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
111 110 iuneq2dv ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) → ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
112 94 111 syl5eq ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) → ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) )
113 112 eqeq2d ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) ↔ 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
114 113 biimprd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) → 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) ) )
115 114 ralimdva ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ) → ( ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) ) )
116 115 impr ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) )
117 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑚 ‘ 𝑛 ) = ( 𝑚 ‘ 𝑘 ) )
118 117 iuneq1d ⊢ ( 𝑛 = 𝑘 → ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) )
119 simpl ⊢ ( ( 𝑛 = 𝑘 ∧ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ) → 𝑛 = 𝑘 )
120 119 oveq2d ⊢ ( ( 𝑛 = 𝑘 ∧ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ) → ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑘 ) )
121 120 iuneq2dv ⊢ ( 𝑛 = 𝑘 → ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑘 ) )
122 118 121 eqtrd ⊢ ( 𝑛 = 𝑘 → ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑘 ) )
123 122 eqeq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) ↔ 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑘 ) ) )
124 123 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑛 ) ↔ ∀ 𝑘 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑘 ) )
125 116 124 sylib ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∀ 𝑘 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ ( 𝑚 ‘ 𝑘 ) ( 𝑡 ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) 𝑘 ) )
126 1 84 85 86 87 92 125 heiborlem10 ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ∧ ( 𝑟 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑟 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 )
127 126 exp32 ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( 𝑟 ⊆ 𝐽 → ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) ) )
128 83 127 syl5 ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( 𝑟 ∈ 𝒫 𝐽 → ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) ) )
129 128 ralrimiv ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∀ 𝑟 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) )
130 129 ex ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) → ∀ 𝑟 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) ) )
131 130 exlimdv ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( ∃ 𝑚 ( 𝑚 : ℕ0 ⟶ ( 𝒫 ∪ 𝐽 ∩ Fin ) ∧ ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝑚 ‘ 𝑛 ) ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑛 ) ) ) ) → ∀ 𝑟 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) ) )
132 82 131 syld ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( 𝐷 ∈ ( TotBnd ‘ 𝑋 ) → ∀ 𝑟 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) ) )
133 132 imp ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ) → ∀ 𝑟 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) )
134 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
135 134 iscmp ⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑟 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑟 → ∃ 𝑣 ∈ ( 𝒫 𝑟 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) ) )
136 8 133 135 sylanbrc ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ) → 𝐽 ∈ Comp )
137 4 136 jca ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ) → ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 ∈ Comp ) )
138 2 137 impbii ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 ∈ Comp ) ↔ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd ‘ 𝑋 ) ) )