This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( ( 𝐷 ∈ ( 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 ‘ 𝑋 ) ) )