Metamath Proof Explorer

Theorem heibor1

Description: One half of heibor , that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet and total boundedness here, which follows trivially from the fact that the set of all r -balls is an open cover of X , so finitely many cover X . (Contributed by Jeff Madsen, 16-Jan-2014)

Ref Expression
Hypothesis heibor.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
Assertion heibor1 ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd β€˜ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 heibor.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
2 simpll ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ ( π‘₯ ∈ ( Cau β€˜ 𝐷 ) ∧ π‘₯ : β„• ⟢ 𝑋 ) ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
3 simplr ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ ( π‘₯ ∈ ( Cau β€˜ 𝐷 ) ∧ π‘₯ : β„• ⟢ 𝑋 ) ) β†’ 𝐽 ∈ Comp )
4 simprl ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ ( π‘₯ ∈ ( Cau β€˜ 𝐷 ) ∧ π‘₯ : β„• ⟢ 𝑋 ) ) β†’ π‘₯ ∈ ( Cau β€˜ 𝐷 ) )
5 simprr ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ ( π‘₯ ∈ ( Cau β€˜ 𝐷 ) ∧ π‘₯ : β„• ⟢ 𝑋 ) ) β†’ π‘₯ : β„• ⟢ 𝑋 )
6 1 2 3 4 5 heibor1lem ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ ( π‘₯ ∈ ( Cau β€˜ 𝐷 ) ∧ π‘₯ : β„• ⟢ 𝑋 ) ) β†’ π‘₯ ∈ dom ( ⇝𝑑 β€˜ 𝐽 ) )
7 6 expr ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘₯ ∈ ( Cau β€˜ 𝐷 ) ) β†’ ( π‘₯ : β„• ⟢ 𝑋 β†’ π‘₯ ∈ dom ( ⇝𝑑 β€˜ 𝐽 ) ) )
8 7 ralrimiva ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ βˆ€ π‘₯ ∈ ( Cau β€˜ 𝐷 ) ( π‘₯ : β„• ⟢ 𝑋 β†’ π‘₯ ∈ dom ( ⇝𝑑 β€˜ 𝐽 ) ) )
9 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
10 1zzd ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ 1 ∈ β„€ )
11 simpl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
12 9 1 10 11 iscmet3 ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ↔ βˆ€ π‘₯ ∈ ( Cau β€˜ 𝐷 ) ( π‘₯ : β„• ⟢ 𝑋 β†’ π‘₯ ∈ dom ( ⇝𝑑 β€˜ 𝐽 ) ) ) )
13 8 12 mpbird ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ 𝐷 ∈ ( CMet β€˜ 𝑋 ) )
14 simplr ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝐽 ∈ Comp )
15 metxmet ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
16 id ⊒ ( 𝑧 ∈ 𝑋 β†’ 𝑧 ∈ 𝑋 )
17 rpxr ⊒ ( π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ* )
18 1 blopn ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ* ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ 𝐽 )
19 15 16 17 18 syl3an ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ 𝐽 )
20 19 3com23 ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ∧ 𝑧 ∈ 𝑋 ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ 𝐽 )
21 20 3expa ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ 𝐽 )
22 eleq1a ⊒ ( ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ 𝐽 β†’ ( 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) β†’ 𝑦 ∈ 𝐽 ) )
23 21 22 syl ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) β†’ ( 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) β†’ 𝑦 ∈ 𝐽 ) )
24 23 rexlimdva ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) β†’ 𝑦 ∈ 𝐽 ) )
25 24 adantlr ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) β†’ 𝑦 ∈ 𝐽 ) )
26 25 abssdv ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } βŠ† 𝐽 )
27 15 ad2antrr ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
28 1 mopnuni ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝑋 = βˆͺ 𝐽 )
29 27 28 syl ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑋 = βˆͺ 𝐽 )
30 blcntr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑧 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
31 15 30 syl3an1 ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑧 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
32 31 3com23 ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ∧ 𝑧 ∈ 𝑋 ) β†’ 𝑧 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
33 32 3expa ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) β†’ 𝑧 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
34 ovex ⊒ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ V
35 34 elabrex ⊒ ( 𝑧 ∈ 𝑋 β†’ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
36 35 adantl ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
37 elunii ⊒ ( ( 𝑧 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) β†’ 𝑧 ∈ βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
38 33 36 37 syl2anc ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑋 ) β†’ 𝑧 ∈ βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
39 38 ralrimiva ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆ€ 𝑧 ∈ 𝑋 𝑧 ∈ βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
40 39 adantlr ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆ€ 𝑧 ∈ 𝑋 𝑧 ∈ βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
41 nfcv ⊒ β„² 𝑧 𝑋
42 nfre1 ⊒ β„² 𝑧 βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ )
43 42 nfab ⊒ β„² 𝑧 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) }
44 43 nfuni ⊒ β„² 𝑧 βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) }
45 41 44 dfss3f ⊒ ( 𝑋 βŠ† βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ↔ βˆ€ 𝑧 ∈ 𝑋 𝑧 ∈ βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
46 40 45 sylibr ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑋 βŠ† βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
47 29 46 eqsstrrd ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆͺ 𝐽 βŠ† βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
48 26 unissd ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } βŠ† βˆͺ 𝐽 )
49 47 48 eqssd ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆͺ 𝐽 = βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
50 eqid ⊒ βˆͺ 𝐽 = βˆͺ 𝐽
51 50 cmpcov ⊒ ( ( 𝐽 ∈ Comp ∧ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } βŠ† 𝐽 ∧ βˆͺ 𝐽 = βˆͺ { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) β†’ βˆƒ π‘₯ ∈ ( 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∩ Fin ) βˆͺ 𝐽 = βˆͺ π‘₯ )
52 14 26 49 51 syl3anc ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆƒ π‘₯ ∈ ( 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∩ Fin ) βˆͺ 𝐽 = βˆͺ π‘₯ )
53 elin ⊒ ( π‘₯ ∈ ( 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∩ Fin ) ↔ ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ π‘₯ ∈ Fin ) )
54 ancom ⊒ ( ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ π‘₯ ∈ Fin ) ↔ ( π‘₯ ∈ Fin ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) )
55 53 54 bitri ⊒ ( π‘₯ ∈ ( 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∩ Fin ) ↔ ( π‘₯ ∈ Fin ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) )
56 55 anbi1i ⊒ ( ( π‘₯ ∈ ( 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∩ Fin ) ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) ↔ ( ( π‘₯ ∈ Fin ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) )
57 anass ⊒ ( ( ( π‘₯ ∈ Fin ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) ↔ ( π‘₯ ∈ Fin ∧ ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) ) )
58 56 57 bitri ⊒ ( ( π‘₯ ∈ ( 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∩ Fin ) ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) ↔ ( π‘₯ ∈ Fin ∧ ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) ) )
59 58 rexbii2 ⊒ ( βˆƒ π‘₯ ∈ ( 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∩ Fin ) βˆͺ 𝐽 = βˆͺ π‘₯ ↔ βˆƒ π‘₯ ∈ Fin ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) )
60 52 59 sylib ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆƒ π‘₯ ∈ Fin ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) )
61 ancom ⊒ ( ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) ↔ ( βˆͺ 𝐽 = βˆͺ π‘₯ ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) )
62 eqcom ⊒ ( βˆͺ π‘₯ = 𝑋 ↔ 𝑋 = βˆͺ π‘₯ )
63 29 eqeq1d ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑋 = βˆͺ π‘₯ ↔ βˆͺ 𝐽 = βˆͺ π‘₯ ) )
64 62 63 bitr2id ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( βˆͺ 𝐽 = βˆͺ π‘₯ ↔ βˆͺ π‘₯ = 𝑋 ) )
65 64 anbi1d ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( βˆͺ 𝐽 = βˆͺ π‘₯ ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) ↔ ( βˆͺ π‘₯ = 𝑋 ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) ) )
66 61 65 bitrid ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) ↔ ( βˆͺ π‘₯ = 𝑋 ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) ) )
67 elpwi ⊒ ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } β†’ π‘₯ βŠ† { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } )
68 ssabral ⊒ ( π‘₯ βŠ† { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ↔ βˆ€ 𝑦 ∈ π‘₯ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
69 67 68 sylib ⊒ ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } β†’ βˆ€ 𝑦 ∈ π‘₯ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
70 69 anim2i ⊒ ( ( βˆͺ π‘₯ = 𝑋 ∧ π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ) β†’ ( βˆͺ π‘₯ = 𝑋 ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ) )
71 66 70 syl6bi ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) β†’ ( βˆͺ π‘₯ = 𝑋 ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ) ) )
72 71 reximdv ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( βˆƒ π‘₯ ∈ Fin ( π‘₯ ∈ 𝒫 { 𝑦 ∣ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) } ∧ βˆͺ 𝐽 = βˆͺ π‘₯ ) β†’ βˆƒ π‘₯ ∈ Fin ( βˆͺ π‘₯ = 𝑋 ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ) ) )
73 60 72 mpd ⊒ ( ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆƒ π‘₯ ∈ Fin ( βˆͺ π‘₯ = 𝑋 ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ) )
74 73 ralrimiva ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ βˆ€ π‘Ÿ ∈ ℝ+ βˆƒ π‘₯ ∈ Fin ( βˆͺ π‘₯ = 𝑋 ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ) )
75 istotbnd ⊒ ( 𝐷 ∈ ( TotBnd β€˜ 𝑋 ) ↔ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ βˆ€ π‘Ÿ ∈ ℝ+ βˆƒ π‘₯ ∈ Fin ( βˆͺ π‘₯ = 𝑋 ∧ βˆ€ 𝑦 ∈ π‘₯ βˆƒ 𝑧 ∈ 𝑋 𝑦 = ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) ) ) )
76 11 74 75 sylanbrc ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ 𝐷 ∈ ( TotBnd β€˜ 𝑋 ) )
77 13 76 jca ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐽 ∈ Comp ) β†’ ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝐷 ∈ ( TotBnd β€˜ 𝑋 ) ) )