Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heibor Structured version   Visualization version   GIF version

Theorem heibor 33945
Description: Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 33934 and heiborlem1 33935 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jan-2014.)
Hypothesis
Ref Expression
heibor.1 𝐽 = (MetOpen‘𝐷)
Assertion
Ref Expression
heibor ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))

Proof of Theorem heibor
Dummy variables 𝑡 𝑛 𝑦 𝑘 𝑟 𝑢 𝑚 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 heibor.1 . . 3 𝐽 = (MetOpen‘𝐷)
21heibor1 33934 . 2 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) → (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))
3 cmetmet 23296 . . . 4 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
43adantr 466 . . 3 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐷 ∈ (Met‘𝑋))
5 metxmet 22352 . . . . . 6 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
61mopntop 22458 . . . . . 6 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
73, 5, 63syl 18 . . . . 5 (𝐷 ∈ (CMet‘𝑋) → 𝐽 ∈ Top)
87adantr 466 . . . 4 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐽 ∈ Top)
9 istotbnd 33893 . . . . . . . . . . . . 13 (𝐷 ∈ (TotBnd‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑟 ∈ ℝ+𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟))))
109simprbi 484 . . . . . . . . . . . 12 (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑟 ∈ ℝ+𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)))
11 2nn 11385 . . . . . . . . . . . . . . 15 2 ∈ ℕ
12 nnexpcl 13073 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
1311, 12mpan 670 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → (2↑𝑛) ∈ ℕ)
1413nnrpd 12066 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 → (2↑𝑛) ∈ ℝ+)
1514rpreccld 12078 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 → (1 / (2↑𝑛)) ∈ ℝ+)
16 oveq2 6799 . . . . . . . . . . . . . . . . . 18 (𝑟 = (1 / (2↑𝑛)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
1716eqeq2d 2781 . . . . . . . . . . . . . . . . 17 (𝑟 = (1 / (2↑𝑛)) → (𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
1817rexbidv 3200 . . . . . . . . . . . . . . . 16 (𝑟 = (1 / (2↑𝑛)) → (∃𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
1918ralbidv 3135 . . . . . . . . . . . . . . 15 (𝑟 = (1 / (2↑𝑛)) → (∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
2019anbi2d 614 . . . . . . . . . . . . . 14 (𝑟 = (1 / (2↑𝑛)) → (( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ↔ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
2120rexbidv 3200 . . . . . . . . . . . . 13 (𝑟 = (1 / (2↑𝑛)) → (∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ↔ ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
2221rspccva 3459 . . . . . . . . . . . 12 ((∀𝑟 ∈ ℝ+𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ∧ (1 / (2↑𝑛)) ∈ ℝ+) → ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
2310, 15, 22syl2an 583 . . . . . . . . . . 11 ((𝐷 ∈ (TotBnd‘𝑋) ∧ 𝑛 ∈ ℕ0) → ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
2423expcom 398 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
2524adantl 467 . . . . . . . . 9 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
26 oveq1 6798 . . . . . . . . . . . . . . 15 (𝑦 = (𝑚𝑣) → (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
2726eqeq2d 2781 . . . . . . . . . . . . . 14 (𝑦 = (𝑚𝑣) → (𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
2827ac6sfi 8358 . . . . . . . . . . . . 13 ((𝑢 ∈ Fin ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑚(𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
2928adantrl 695 . . . . . . . . . . . 12 ((𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∃𝑚(𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
3029adantl 467 . . . . . . . . . . 11 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ∃𝑚(𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
31 simp3l 1243 . . . . . . . . . . . . . . . . . . 19 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑚:𝑢𝑋)
32 frn 6191 . . . . . . . . . . . . . . . . . . 19 (𝑚:𝑢𝑋 → ran 𝑚𝑋)
3331, 32syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚𝑋)
341mopnuni 22459 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
353, 5, 343syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (CMet‘𝑋) → 𝑋 = 𝐽)
3635adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → 𝑋 = 𝐽)
37363ad2ant1 1127 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑋 = 𝐽)
3833, 37sseqtrd 3790 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 𝐽)
391fvexi 6341 . . . . . . . . . . . . . . . . . . 19 𝐽 ∈ V
4039uniex 7098 . . . . . . . . . . . . . . . . . 18 𝐽 ∈ V
4140elpw2 4959 . . . . . . . . . . . . . . . . 17 (ran 𝑚 ∈ 𝒫 𝐽 ↔ ran 𝑚 𝐽)
4238, 41sylibr 224 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ 𝒫 𝐽)
43 simp2l 1241 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑢 ∈ Fin)
44 ffn 6183 . . . . . . . . . . . . . . . . . . 19 (𝑚:𝑢𝑋𝑚 Fn 𝑢)
45 dffn4 6260 . . . . . . . . . . . . . . . . . . 19 (𝑚 Fn 𝑢𝑚:𝑢onto→ran 𝑚)
4644, 45sylib 208 . . . . . . . . . . . . . . . . . 18 (𝑚:𝑢𝑋𝑚:𝑢onto→ran 𝑚)
47 fofi 8406 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ Fin ∧ 𝑚:𝑢onto→ran 𝑚) → ran 𝑚 ∈ Fin)
4846, 47sylan2 580 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ Fin ∧ 𝑚:𝑢𝑋) → ran 𝑚 ∈ Fin)
4943, 31, 48syl2anc 573 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ Fin)
5042, 49elind 3949 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ (𝒫 𝐽 ∩ Fin))
5126eleq2d 2836 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑚𝑣) → (𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑟 ∈ ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
5251rexrn 6502 . . . . . . . . . . . . . . . . . . 19 (𝑚 Fn 𝑢 → (∃𝑦 ∈ ran 𝑚 𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑣𝑢 𝑟 ∈ ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
53 eliun 4658 . . . . . . . . . . . . . . . . . . 19 (𝑟 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑦 ∈ ran 𝑚 𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
54 eliun 4658 . . . . . . . . . . . . . . . . . . 19 (𝑟 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑣𝑢 𝑟 ∈ ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
5552, 53, 543bitr4g 303 . . . . . . . . . . . . . . . . . 18 (𝑚 Fn 𝑢 → (𝑟 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑟 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
5655eqrdv 2769 . . . . . . . . . . . . . . . . 17 (𝑚 Fn 𝑢 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
5731, 44, 563syl 18 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
58 simp3r 1244 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
59 uniiun 4707 . . . . . . . . . . . . . . . . . 18 𝑢 = 𝑣𝑢 𝑣
60 iuneq2 4671 . . . . . . . . . . . . . . . . . 18 (∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))) → 𝑣𝑢 𝑣 = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
6159, 60syl5eq 2817 . . . . . . . . . . . . . . . . 17 (∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))) → 𝑢 = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
6258, 61syl 17 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑢 = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
63 simp2r 1242 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑢 = 𝑋)
6457, 62, 633eqtr2rd 2812 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑋 = 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
65 iuneq1 4668 . . . . . . . . . . . . . . . . 17 (𝑡 = ran 𝑚 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
6665eqeq2d 2781 . . . . . . . . . . . . . . . 16 (𝑡 = ran 𝑚 → (𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑋 = 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
6766rspcev 3460 . . . . . . . . . . . . . . 15 ((ran 𝑚 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑋 = 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
6850, 64, 67syl2anc 573 . . . . . . . . . . . . . 14 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
69683expia 1114 . . . . . . . . . . . . 13 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋)) → ((𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7069adantrrr 704 . . . . . . . . . . . 12 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ((𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7170exlimdv 2013 . . . . . . . . . . 11 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → (∃𝑚(𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7230, 71mpd 15 . . . . . . . . . 10 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
7372rexlimdvaa 3180 . . . . . . . . 9 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7425, 73syld 47 . . . . . . . 8 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7574ralrimdva 3118 . . . . . . 7 (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑛 ∈ ℕ0𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7640pwex 4981 . . . . . . . . 9 𝒫 𝐽 ∈ V
7776inex1 4933 . . . . . . . 8 (𝒫 𝐽 ∩ Fin) ∈ V
78 nn0ennn 12979 . . . . . . . . 9 0 ≈ ℕ
79 nnenom 12980 . . . . . . . . 9 ℕ ≈ ω
8078, 79entri 8161 . . . . . . . 8 0 ≈ ω
81 iuneq1 4668 . . . . . . . . 9 (𝑡 = (𝑚𝑛) → 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
8281eqeq2d 2781 . . . . . . . 8 (𝑡 = (𝑚𝑛) → (𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
8377, 80, 82axcc4 9461 . . . . . . 7 (∀𝑛 ∈ ℕ0𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) → ∃𝑚(𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
8475, 83syl6 35 . . . . . 6 (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑚(𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
85 elpwi 4307 . . . . . . . . . 10 (𝑟 ∈ 𝒫 𝐽𝑟𝐽)
86 eqid 2771 . . . . . . . . . . . 12 {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 𝑣} = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 𝑣}
87 eqid 2771 . . . . . . . . . . . 12 {⟨𝑡, 𝑘⟩ ∣ (𝑘 ∈ ℕ0𝑡 ∈ (𝑚𝑘) ∧ (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘) ∈ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 𝑣})} = {⟨𝑡, 𝑘⟩ ∣ (𝑘 ∈ ℕ0𝑡 ∈ (𝑚𝑘) ∧ (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘) ∈ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 𝑣})}
88 eqid 2771 . . . . . . . . . . . 12 (𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) = (𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
89 simpl 468 . . . . . . . . . . . 12 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → 𝐷 ∈ (CMet‘𝑋))
9035pweqd 4302 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (CMet‘𝑋) → 𝒫 𝑋 = 𝒫 𝐽)
9190ineq1d 3964 . . . . . . . . . . . . . . 15 (𝐷 ∈ (CMet‘𝑋) → (𝒫 𝑋 ∩ Fin) = (𝒫 𝐽 ∩ Fin))
9291feq3d 6170 . . . . . . . . . . . . . 14 (𝐷 ∈ (CMet‘𝑋) → (𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin) ↔ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)))
9392biimpar 463 . . . . . . . . . . . . 13 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) → 𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9493adantrr 696 . . . . . . . . . . . 12 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin))
95 oveq1 6798 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑦 → (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))
9695cbviunv 4693 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑦 ∈ (𝑚𝑛)(𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)
97 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) → 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin))
98 inss1 3981 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝒫 𝐽 ∩ Fin) ⊆ 𝒫 𝐽
9998, 90syl5sseqr 3803 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐷 ∈ (CMet‘𝑋) → (𝒫 𝐽 ∩ Fin) ⊆ 𝒫 𝑋)
100 fss 6194 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ (𝒫 𝐽 ∩ Fin) ⊆ 𝒫 𝑋) → 𝑚:ℕ0⟶𝒫 𝑋)
10197, 99, 100syl2anr 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) → 𝑚:ℕ0⟶𝒫 𝑋)
102101ffvelrnda 6500 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → (𝑚𝑛) ∈ 𝒫 𝑋)
103102elpwid 4309 . . . . . . . . . . . . . . . . . . . . 21 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → (𝑚𝑛) ⊆ 𝑋)
104103sselda 3752 . . . . . . . . . . . . . . . . . . . 20 ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑦 ∈ (𝑚𝑛)) → 𝑦𝑋)
105 simplr 752 . . . . . . . . . . . . . . . . . . . 20 ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑦 ∈ (𝑚𝑛)) → 𝑛 ∈ ℕ0)
106 oveq1 6798 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑦 → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (𝑦(ball‘𝐷)(1 / (2↑𝑚))))
107 oveq2 6799 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛))
108107oveq2d 6807 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 → (1 / (2↑𝑚)) = (1 / (2↑𝑛)))
109108oveq2d 6807 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑦(ball‘𝐷)(1 / (2↑𝑚))) = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
110 ovex 6821 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ∈ V
111106, 109, 88, 110ovmpt2 6941 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑋𝑛 ∈ ℕ0) → (𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
112104, 105, 111syl2anc 573 . . . . . . . . . . . . . . . . . . 19 ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑦 ∈ (𝑚𝑛)) → (𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
113112iuneq2dv 4676 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → 𝑦 ∈ (𝑚𝑛)(𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
11496, 113syl5eq 2817 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
115114eqeq2d 2781 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → (𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
116115biimprd 238 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → (𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))) → 𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)))
117116ralimdva 3111 . . . . . . . . . . . . . 14 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) → (∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))) → ∀𝑛 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)))
118117impr 442 . . . . . . . . . . . . 13 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑛 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))
119 fveq2 6330 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑚𝑛) = (𝑚𝑘))
120119iuneq1d 4679 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))
121 simpl 468 . . . . . . . . . . . . . . . . . 18 ((𝑛 = 𝑘𝑡 ∈ (𝑚𝑘)) → 𝑛 = 𝑘)
122121oveq2d 6807 . . . . . . . . . . . . . . . . 17 ((𝑛 = 𝑘𝑡 ∈ (𝑚𝑘)) → (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
123122iuneq2dv 4676 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
124120, 123eqtrd 2805 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
125124eqeq2d 2781 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ 𝑋 = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)))
126125cbvralv 3320 . . . . . . . . . . . . 13 (∀𝑛 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ ∀𝑘 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
127118, 126sylib 208 . . . . . . . . . . . 12 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑘 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
1281, 86, 87, 88, 89, 94, 127heiborlem10 33944 . . . . . . . . . . 11 (((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) ∧ (𝑟𝐽 𝐽 = 𝑟)) → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)
129128exp32 407 . . . . . . . . . 10 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → (𝑟𝐽 → ( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
13085, 129syl5 34 . . . . . . . . 9 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → (𝑟 ∈ 𝒫 𝐽 → ( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
131130ralrimiv 3114 . . . . . . . 8 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣))
132131ex 397 . . . . . . 7 (𝐷 ∈ (CMet‘𝑋) → ((𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
133132exlimdv 2013 . . . . . 6 (𝐷 ∈ (CMet‘𝑋) → (∃𝑚(𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
13484, 133syld 47 . . . . 5 (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
135134imp 393 . . . 4 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣))
136 eqid 2771 . . . . 5 𝐽 = 𝐽
137136iscmp 21405 . . . 4 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
1388, 135, 137sylanbrc 572 . . 3 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐽 ∈ Comp)
1394, 138jca 501 . 2 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → (𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp))
1402, 139impbii 199 1 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  {cab 2757  wral 3061  wrex 3062  cin 3722  wss 3723  𝒫 cpw 4297   cuni 4574   ciun 4654  {copab 4846  ran crn 5250   Fn wfn 6024  wf 6025  ontowfo 6027  cfv 6029  (class class class)co 6791  cmpt2 6793  ωcom 7210  Fincfn 8107  1c1 10137   / cdiv 10884  cn 11220  2c2 11270  0cn0 11492  +crp 12028  cexp 13060  ∞Metcxmt 19939  Metcme 19940  ballcbl 19941  MetOpencmopn 19944  Topctop 20911  Compccmp 21403  CMetcms 23264  TotBndctotbnd 33890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-inf2 8700  ax-cc 9457  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213  ax-pre-sup 10214
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-isom 6038  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-2o 7712  df-oadd 7715  df-omul 7716  df-er 7894  df-map 8009  df-pm 8010  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-fi 8471  df-sup 8502  df-inf 8503  df-oi 8569  df-card 8963  df-acn 8966  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-div 10885  df-nn 11221  df-2 11279  df-3 11280  df-n0 11493  df-z 11578  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12144  df-xadd 12145  df-xmul 12146  df-ico 12379  df-icc 12380  df-fz 12527  df-fl 12794  df-seq 13002  df-exp 13061  df-cj 14040  df-re 14041  df-im 14042  df-sqrt 14176  df-abs 14177  df-clim 14420  df-rlim 14421  df-rest 16284  df-topgen 16305  df-psmet 19946  df-xmet 19947  df-met 19948  df-bl 19949  df-mopn 19950  df-fbas 19951  df-fg 19952  df-top 20912  df-topon 20929  df-bases 20964  df-cld 21037  df-ntr 21038  df-cls 21039  df-nei 21116  df-lm 21247  df-haus 21333  df-cmp 21404  df-fil 21863  df-fm 21955  df-flim 21956  df-flf 21957  df-cfil 23265  df-cau 23266  df-cmet 23267  df-totbnd 33892
This theorem is referenced by:  rrnheibor  33961
  Copyright terms: Public domain W3C validator