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

Theorem heibor 35217
 Description: Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 35206 and heiborlem1 35207 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 35206 . 2 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) → (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))
3 cmetmet 23888 . . . 4 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
43adantr 484 . . 3 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐷 ∈ (Met‘𝑋))
5 metxmet 22939 . . . . . 6 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
61mopntop 23045 . . . . . 6 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
73, 5, 63syl 18 . . . . 5 (𝐷 ∈ (CMet‘𝑋) → 𝐽 ∈ Top)
87adantr 484 . . . 4 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐽 ∈ Top)
9 istotbnd 35165 . . . . . . . . . . . . 13 (𝐷 ∈ (TotBnd‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑟 ∈ ℝ+𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟))))
109simprbi 500 . . . . . . . . . . . 12 (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑟 ∈ ℝ+𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)))
11 2nn 11698 . . . . . . . . . . . . . . 15 2 ∈ ℕ
12 nnexpcl 13438 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
1311, 12mpan 689 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → (2↑𝑛) ∈ ℕ)
1413nnrpd 12417 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 → (2↑𝑛) ∈ ℝ+)
1514rpreccld 12429 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 → (1 / (2↑𝑛)) ∈ ℝ+)
16 oveq2 7148 . . . . . . . . . . . . . . . . . 18 (𝑟 = (1 / (2↑𝑛)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
1716eqeq2d 2833 . . . . . . . . . . . . . . . . 17 (𝑟 = (1 / (2↑𝑛)) → (𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
1817rexbidv 3283 . . . . . . . . . . . . . . . 16 (𝑟 = (1 / (2↑𝑛)) → (∃𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
1918ralbidv 3187 . . . . . . . . . . . . . . 15 (𝑟 = (1 / (2↑𝑛)) → (∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
2019anbi2d 631 . . . . . . . . . . . . . 14 (𝑟 = (1 / (2↑𝑛)) → (( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ↔ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
2120rexbidv 3283 . . . . . . . . . . . . 13 (𝑟 = (1 / (2↑𝑛)) → (∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ↔ ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
2221rspccva 3597 . . . . . . . . . . . 12 ((∀𝑟 ∈ ℝ+𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ∧ (1 / (2↑𝑛)) ∈ ℝ+) → ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
2310, 15, 22syl2an 598 . . . . . . . . . . 11 ((𝐷 ∈ (TotBnd‘𝑋) ∧ 𝑛 ∈ ℕ0) → ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
2423expcom 417 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
2524adantl 485 . . . . . . . . 9 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
26 oveq1 7147 . . . . . . . . . . . . . . 15 (𝑦 = (𝑚𝑣) → (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
2726eqeq2d 2833 . . . . . . . . . . . . . 14 (𝑦 = (𝑚𝑣) → (𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
2827ac6sfi 8750 . . . . . . . . . . . . 13 ((𝑢 ∈ Fin ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑚(𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
2928adantrl 715 . . . . . . . . . . . 12 ((𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∃𝑚(𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
3029adantl 485 . . . . . . . . . . 11 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ∃𝑚(𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
31 simp3l 1198 . . . . . . . . . . . . . . . . . . 19 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑚:𝑢𝑋)
3231frnd 6501 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚𝑋)
331mopnuni 23046 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
343, 5, 333syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (CMet‘𝑋) → 𝑋 = 𝐽)
3534adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → 𝑋 = 𝐽)
36353ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑋 = 𝐽)
3732, 36sseqtrd 3982 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 𝐽)
381fvexi 6666 . . . . . . . . . . . . . . . . . . 19 𝐽 ∈ V
3938uniex 7452 . . . . . . . . . . . . . . . . . 18 𝐽 ∈ V
4039elpw2 5224 . . . . . . . . . . . . . . . . 17 (ran 𝑚 ∈ 𝒫 𝐽 ↔ ran 𝑚 𝐽)
4137, 40sylibr 237 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ 𝒫 𝐽)
42 simp2l 1196 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑢 ∈ Fin)
43 ffn 6494 . . . . . . . . . . . . . . . . . . 19 (𝑚:𝑢𝑋𝑚 Fn 𝑢)
44 dffn4 6578 . . . . . . . . . . . . . . . . . . 19 (𝑚 Fn 𝑢𝑚:𝑢onto→ran 𝑚)
4543, 44sylib 221 . . . . . . . . . . . . . . . . . 18 (𝑚:𝑢𝑋𝑚:𝑢onto→ran 𝑚)
46 fofi 8798 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ Fin ∧ 𝑚:𝑢onto→ran 𝑚) → ran 𝑚 ∈ Fin)
4745, 46sylan2 595 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ Fin ∧ 𝑚:𝑢𝑋) → ran 𝑚 ∈ Fin)
4842, 31, 47syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ Fin)
4941, 48elind 4145 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ (𝒫 𝐽 ∩ Fin))
5026eleq2d 2899 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑚𝑣) → (𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑟 ∈ ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
5150rexrn 6835 . . . . . . . . . . . . . . . . . . 19 (𝑚 Fn 𝑢 → (∃𝑦 ∈ ran 𝑚 𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑣𝑢 𝑟 ∈ ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
52 eliun 4898 . . . . . . . . . . . . . . . . . . 19 (𝑟 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑦 ∈ ran 𝑚 𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
53 eliun 4898 . . . . . . . . . . . . . . . . . . 19 (𝑟 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑣𝑢 𝑟 ∈ ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
5451, 52, 533bitr4g 317 . . . . . . . . . . . . . . . . . 18 (𝑚 Fn 𝑢 → (𝑟 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑟 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))))
5554eqrdv 2820 . . . . . . . . . . . . . . . . 17 (𝑚 Fn 𝑢 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
5631, 43, 553syl 18 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
57 simp3r 1199 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
58 uniiun 4957 . . . . . . . . . . . . . . . . . 18 𝑢 = 𝑣𝑢 𝑣
59 iuneq2 4913 . . . . . . . . . . . . . . . . . 18 (∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))) → 𝑣𝑢 𝑣 = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
6058, 59syl5eq 2869 . . . . . . . . . . . . . . . . 17 (∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))) → 𝑢 = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
6157, 60syl 17 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑢 = 𝑣𝑢 ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))
62 simp2r 1197 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑢 = 𝑋)
6356, 61, 623eqtr2rd 2864 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑋 = 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
64 iuneq1 4910 . . . . . . . . . . . . . . . 16 (𝑡 = ran 𝑚 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
6564rspceeqv 3613 . . . . . . . . . . . . . . 15 ((ran 𝑚 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑋 = 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
6649, 63, 65syl2anc 587 . . . . . . . . . . . . . 14 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋) ∧ (𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
67663expia 1118 . . . . . . . . . . . . 13 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ 𝑢 = 𝑋)) → ((𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
6867adantrrr 724 . . . . . . . . . . . 12 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ((𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
6968exlimdv 1934 . . . . . . . . . . 11 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → (∃𝑚(𝑚:𝑢𝑋 ∧ ∀𝑣𝑢 𝑣 = ((𝑚𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7030, 69mpd 15 . . . . . . . . . 10 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
7170rexlimdvaa 3271 . . . . . . . . 9 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (∃𝑢 ∈ Fin ( 𝑢 = 𝑋 ∧ ∀𝑣𝑢𝑦𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7225, 71syld 47 . . . . . . . 8 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7372ralrimdva 3179 . . . . . . 7 (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑛 ∈ ℕ0𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
7439pwex 5258 . . . . . . . . 9 𝒫 𝐽 ∈ V
7574inex1 5197 . . . . . . . 8 (𝒫 𝐽 ∩ Fin) ∈ V
76 nn0ennn 13342 . . . . . . . . 9 0 ≈ ℕ
77 nnenom 13343 . . . . . . . . 9 ℕ ≈ ω
7876, 77entri 8550 . . . . . . . 8 0 ≈ ω
79 iuneq1 4910 . . . . . . . . 9 (𝑡 = (𝑚𝑛) → 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
8079eqeq2d 2833 . . . . . . . 8 (𝑡 = (𝑚𝑛) → (𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
8175, 78, 80axcc4 9850 . . . . . . 7 (∀𝑛 ∈ ℕ0𝑡 ∈ (𝒫 𝐽 ∩ Fin)𝑋 = 𝑦𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) → ∃𝑚(𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
8273, 81syl6 35 . . . . . 6 (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑚(𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))))
83 elpwi 4520 . . . . . . . . . 10 (𝑟 ∈ 𝒫 𝐽𝑟𝐽)
84 eqid 2822 . . . . . . . . . . . 12 {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 𝑣} = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 𝑣}
85 eqid 2822 . . . . . . . . . . . 12 {⟨𝑡, 𝑘⟩ ∣ (𝑘 ∈ ℕ0𝑡 ∈ (𝑚𝑘) ∧ (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘) ∈ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 𝑣})} = {⟨𝑡, 𝑘⟩ ∣ (𝑘 ∈ ℕ0𝑡 ∈ (𝑚𝑘) ∧ (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘) ∈ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 𝑣})}
86 eqid 2822 . . . . . . . . . . . 12 (𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) = (𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
87 simpl 486 . . . . . . . . . . . 12 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → 𝐷 ∈ (CMet‘𝑋))
8834pweqd 4530 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (CMet‘𝑋) → 𝒫 𝑋 = 𝒫 𝐽)
8988ineq1d 4162 . . . . . . . . . . . . . . 15 (𝐷 ∈ (CMet‘𝑋) → (𝒫 𝑋 ∩ Fin) = (𝒫 𝐽 ∩ Fin))
9089feq3d 6481 . . . . . . . . . . . . . 14 (𝐷 ∈ (CMet‘𝑋) → (𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin) ↔ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)))
9190biimpar 481 . . . . . . . . . . . . 13 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) → 𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9291adantrr 716 . . . . . . . . . . . 12 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin))
93 oveq1 7147 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑦 → (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))
9493cbviunv 4940 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑦 ∈ (𝑚𝑛)(𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)
95 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) → 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin))
96 inss1 4179 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝒫 𝐽 ∩ Fin) ⊆ 𝒫 𝐽
9796, 88sseqtrrid 3995 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐷 ∈ (CMet‘𝑋) → (𝒫 𝐽 ∩ Fin) ⊆ 𝒫 𝑋)
98 fss 6508 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ (𝒫 𝐽 ∩ Fin) ⊆ 𝒫 𝑋) → 𝑚:ℕ0⟶𝒫 𝑋)
9995, 97, 98syl2anr 599 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) → 𝑚:ℕ0⟶𝒫 𝑋)
10099ffvelrnda 6833 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → (𝑚𝑛) ∈ 𝒫 𝑋)
101100elpwid 4522 . . . . . . . . . . . . . . . . . . . . 21 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → (𝑚𝑛) ⊆ 𝑋)
102101sselda 3942 . . . . . . . . . . . . . . . . . . . 20 ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑦 ∈ (𝑚𝑛)) → 𝑦𝑋)
103 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑦 ∈ (𝑚𝑛)) → 𝑛 ∈ ℕ0)
104 oveq1 7147 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑦 → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (𝑦(ball‘𝐷)(1 / (2↑𝑚))))
105 oveq2 7148 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛))
106105oveq2d 7156 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 → (1 / (2↑𝑚)) = (1 / (2↑𝑛)))
107106oveq2d 7156 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑦(ball‘𝐷)(1 / (2↑𝑚))) = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
108 ovex 7173 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ∈ V
109104, 107, 86, 108ovmpo 7294 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝑋𝑛 ∈ ℕ0) → (𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
110102, 103, 109syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) ∧ 𝑦 ∈ (𝑚𝑛)) → (𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))
111110iuneq2dv 4918 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → 𝑦 ∈ (𝑚𝑛)(𝑦(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
11294, 111syl5eq 2869 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))
113112eqeq2d 2833 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → (𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))
114113biimprd 251 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) ∧ 𝑛 ∈ ℕ0) → (𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))) → 𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)))
115114ralimdva 3169 . . . . . . . . . . . . . 14 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin)) → (∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))) → ∀𝑛 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)))
116115impr 458 . . . . . . . . . . . . 13 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑛 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))
117 fveq2 6652 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → (𝑚𝑛) = (𝑚𝑘))
118117iuneq1d 4921 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))
119 simpl 486 . . . . . . . . . . . . . . . . . 18 ((𝑛 = 𝑘𝑡 ∈ (𝑚𝑘)) → 𝑛 = 𝑘)
120119oveq2d 7156 . . . . . . . . . . . . . . . . 17 ((𝑛 = 𝑘𝑡 ∈ (𝑚𝑘)) → (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
121120iuneq2dv 4918 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
122118, 121eqtrd 2857 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
123122eqeq2d 2833 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ 𝑋 = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)))
124123cbvralvw 3424 . . . . . . . . . . . . 13 (∀𝑛 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑛)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ ∀𝑘 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
125116, 124sylib 221 . . . . . . . . . . . 12 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑘 ∈ ℕ0 𝑋 = 𝑡 ∈ (𝑚𝑘)(𝑡(𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))
1261, 84, 85, 86, 87, 92, 125heiborlem10 35216 . . . . . . . . . . 11 (((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) ∧ (𝑟𝐽 𝐽 = 𝑟)) → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)
127126exp32 424 . . . . . . . . . 10 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → (𝑟𝐽 → ( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
12883, 127syl5 34 . . . . . . . . 9 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → (𝑟 ∈ 𝒫 𝐽 → ( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
129128ralrimiv 3173 . . . . . . . 8 ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣))
130129ex 416 . . . . . . 7 (𝐷 ∈ (CMet‘𝑋) → ((𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
131130exlimdv 1934 . . . . . 6 (𝐷 ∈ (CMet‘𝑋) → (∃𝑚(𝑚:ℕ0⟶(𝒫 𝐽 ∩ Fin) ∧ ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝑚𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
13282, 131syld 47 . . . . 5 (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
133132imp 410 . . . 4 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣))
134 eqid 2822 . . . . 5 𝐽 = 𝐽
135134iscmp 21991 . . . 4 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽( 𝐽 = 𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin) 𝐽 = 𝑣)))
1368, 133, 135sylanbrc 586 . . 3 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐽 ∈ Comp)
1374, 136jca 515 . 2 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → (𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp))
1382, 137impbii 212 1 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2114  {cab 2800  ∀wral 3130  ∃wrex 3131   ∩ cin 3907   ⊆ wss 3908  𝒫 cpw 4511  ∪ cuni 4813  ∪ ciun 4894  {copab 5104  ran crn 5533   Fn wfn 6329  ⟶wf 6330  –onto→wfo 6332  ‘cfv 6334  (class class class)co 7140   ∈ cmpo 7142  ωcom 7565  Fincfn 8496  1c1 10527   / cdiv 11286  ℕcn 11625  2c2 11680  ℕ0cn0 11885  ℝ+crp 12377  ↑cexp 13425  ∞Metcxmet 20074  Metcmet 20075  ballcbl 20076  MetOpencmopn 20079  Topctop 21496  Compccmp 21989  CMetccmet 23856  TotBndctotbnd 35162 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092  ax-cc 9846  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-iin 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-omul 8094  df-er 8276  df-map 8395  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-acn 9359  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ico 12732  df-icc 12733  df-fz 12886  df-fl 13157  df-seq 13365  df-exp 13426  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-clim 14836  df-rlim 14837  df-rest 16687  df-topgen 16708  df-psmet 20081  df-xmet 20082  df-met 20083  df-bl 20084  df-mopn 20085  df-fbas 20086  df-fg 20087  df-top 21497  df-topon 21514  df-bases 21549  df-cld 21622  df-ntr 21623  df-cls 21624  df-nei 21701  df-lm 21832  df-haus 21918  df-cmp 21990  df-fil 22449  df-fm 22541  df-flim 22542  df-flf 22543  df-cfil 23857  df-cau 23858  df-cmet 23859  df-totbnd 35164 This theorem is referenced by:  rrnheibor  35233
 Copyright terms: Public domain W3C validator