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 eqtrid ⊒ ( βˆ€ 𝑣 ∈ 𝑒 𝑣 = ( ( π‘š β€˜ 𝑣 ) ( 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 ffvelcdmda ⊒ ( ( ( 𝐷 ∈ ( 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 eqtrid ⊒ ( ( ( 𝐷 ∈ ( 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 β€˜ 𝑋 ) ) )