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

Theorem pibt2 34250
Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 34247 and pibp21 34248 for the definitions of the relevant properties. This proof uses the axiom of choice. (Contributed by ML, 30-Mar-2021.)
Hypotheses
Ref Expression
pibt2.x 𝑋 = 𝐽
pibt2.19 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(( 𝑥 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
pibt2.21 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 𝑥 ∖ Fin)∃𝑧 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
Assertion
Ref Expression
pibt2 (𝐽𝐶𝐽𝑊)
Distinct variable groups:   𝑦,𝐽,𝑥,𝑧   𝑦,𝑋,𝑥,𝑧
Allowed substitution hints:   𝐶(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)

Proof of Theorem pibt2
Dummy variables 𝑎 𝑏 𝑠 𝑓 𝑛 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pibt2.x . . . 4 𝑋 = 𝐽
2 pibt2.19 . . . 4 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(( 𝑥 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
31, 2pibp19 34247 . . 3 (𝐽𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
43simplbi 498 . 2 (𝐽𝐶𝐽 ∈ Top)
5 eldif 3875 . . . . 5 (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin))
6 selpw 4466 . . . . . . 7 (𝑏 ∈ 𝒫 𝑋𝑏𝑋)
76anbi1i 623 . . . . . 6 ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin))
8 vex 3443 . . . . . . . . . 10 𝑏 ∈ V
9 infinf 9841 . . . . . . . . . 10 (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏))
108, 9ax-mp 5 . . . . . . . . 9 𝑏 ∈ Fin ↔ ω ≼ 𝑏)
118infcntss 8645 . . . . . . . . 9 (ω ≼ 𝑏 → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1210, 11sylbi 218 . . . . . . . 8 𝑏 ∈ Fin → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1312ad2antll 725 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
14 sstr 3903 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑏𝑋) → 𝑎𝑋)
1514ancoms 459 . . . . . . . . . . . . 13 ((𝑏𝑋𝑎𝑏) → 𝑎𝑋)
16 simplr 765 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω)
17 simpll 763 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽𝐶𝑎 ≈ ω))
18 0ss 4276 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∅ ⊆ 𝑎
19 sseq1 3919 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎))
2018, 19mpbiri 259 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
2120adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
221cldlp 21446 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2322adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2421, 23mpbird 258 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
254, 24sylanl1 676 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
2625adantllr 715 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
27 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅)
281cldss 21325 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Clsd‘𝐽) → 𝑎𝑋)
291nlpineqsn 34241 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}))
30 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → (𝑛𝑎) = {𝑝})
3130reximi 3209 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∃𝑛𝐽 (𝑛𝑎) = {𝑝})
3231ralimi 3129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝})
33 vex 3443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑎 ∈ V
34 ineq1 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑓𝑝) → (𝑛𝑎) = ((𝑓𝑝) ∩ 𝑎))
3534eqeq1d 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑓𝑝) → ((𝑛𝑎) = {𝑝} ↔ ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3633, 35ac6s 9759 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3729, 32, 363syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
38 fvineqsnf1 34243 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎1-1𝐽)
39 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})
4038, 39jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4140eximi 1820 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4237, 41syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4328, 42syl3an2 1157 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
444, 43syl3an1 1156 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
45443adant1r 1170 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
46 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → 𝑓:𝑎1-1𝐽)
47 vsnid 4513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑝 ∈ {𝑝}
48 eleq2 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝}))
4947, 48mpbiri 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓𝑝) ∩ 𝑎))
5049elin1d 4102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓𝑝))
5150ralimi 3129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝𝑎 𝑝 ∈ (𝑓𝑝))
52 ralssiun 34240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 𝑝 ∈ (𝑓𝑝) → 𝑎 𝑝𝑎 (𝑓𝑝))
5351, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑎 𝑝𝑎 (𝑓𝑝))
5453adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 𝑝𝑎 (𝑓𝑝))
55 f1fn 6451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:𝑎1-1𝐽𝑓 Fn 𝑎)
56 fniunfv 6878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓 Fn 𝑎 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:𝑎1-1𝐽 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5857adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5954, 58sseqtrd 3934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ran 𝑓)
601cldopn 21327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ (Clsd‘𝐽) → (𝑋𝑎) ∈ 𝐽)
6160ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋𝑎) ∈ 𝐽)
6261anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → ((𝑋𝑎) ∈ 𝐽𝑎 ran 𝑓))
6362ancomd 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))
6428ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎𝑋)
6564anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)))
66 unisng 4766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ∈ 𝐽 {(𝑋𝑎)} = (𝑋𝑎))
6766eqcomd 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) = {(𝑋𝑎)})
68 eqimss 3950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) = {(𝑋𝑎)} → (𝑋𝑎) ⊆ {(𝑋𝑎)})
69 ssun4 4078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ ( ran 𝑓 {(𝑋𝑎)}))
70 uniun 4770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (ran 𝑓 ∪ {(𝑋𝑎)}) = ( ran 𝑓 {(𝑋𝑎)})
7169, 70syl6sseqr 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
7267, 68, 713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
73 ssun3 4077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑎 ran 𝑓𝑎 ⊆ ( ran 𝑓 {(𝑋𝑎)}))
7473, 70syl6sseqr 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ran 𝑓𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}))
75 uncom 4056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎 ∪ (𝑋𝑎)) = ((𝑋𝑎) ∪ 𝑎)
76 undif1 4344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑋𝑎) ∪ 𝑎) = (𝑋𝑎)
7775, 76eqtri 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎 ∪ (𝑋𝑎)) = (𝑋𝑎)
78 ssequn2 4086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎𝑋 ↔ (𝑋𝑎) = 𝑋)
7978biimpi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎𝑋 → (𝑋𝑎) = 𝑋)
8077, 79syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑎𝑋 → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
8180adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
82 unss12 4085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})))
83 unidm 4055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})) = (ran 𝑓 ∪ {(𝑋𝑎)})
8482, 83syl6sseq 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8584adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8681, 85eqsstrrd 3933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8774, 86sylanr1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8872, 87sylanr2 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8988adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
90 f1f 6450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎1-1𝐽𝑓:𝑎𝐽)
91 frn 6395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎𝐽 → ran 𝑓𝐽)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓:𝑎1-1𝐽 → ran 𝑓𝐽)
931topopn 21202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋𝐽)
941difopn 21330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝐽𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9593, 94sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9695snssd 4655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋𝑎)} ⊆ 𝐽)
97 unss12 4085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ (𝐽𝐽))
98 unidm 4055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽𝐽) = 𝐽
9997, 98syl6sseq 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
10092, 96, 99syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
101 uniss 4772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
102101, 1syl6sseqr 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
103100, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
104103adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
10589, 104eqssd 3912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10665, 105syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10763, 106syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10859, 107sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
109108ancom1s 649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
110109ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
11146, 110mpand 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
112111impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
113112adantlrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
1144, 113sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
115 vex 3443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑓 ∈ V
116 f1f1orn 6501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:𝑎1-1𝐽𝑓:𝑎1-1-onto→ran 𝑓)
117 f1oen3g 8380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ V ∧ 𝑓:𝑎1-1-onto→ran 𝑓) → 𝑎 ≈ ran 𝑓)
118115, 116, 117sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓:𝑎1-1𝐽𝑎 ≈ ran 𝑓)
119 enen1 8511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈ ω))
120 endom 8391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ran 𝑓 ≈ ω → ran 𝑓 ≼ ω)
121 snfi 8449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {(𝑋𝑎)} ∈ Fin
122 isfinite 8968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ({(𝑋𝑎)} ∈ Fin ↔ {(𝑋𝑎)} ≺ ω)
123121, 122mpbi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {(𝑋𝑎)} ≺ ω
124 sdomdom 8392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({(𝑋𝑎)} ≺ ω → {(𝑋𝑎)} ≼ ω)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {(𝑋𝑎)} ≼ ω
126 unctb 9480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ran 𝑓 ≼ ω ∧ {(𝑋𝑎)} ≼ ω) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
127120, 125, 126sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (ran 𝑓 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
128119, 127syl6bi 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
129118, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:𝑎1-1𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
130129impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑎 ≈ ω ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
131130adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
132131ad2ant2lr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
133100ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
134133adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
135134adantlrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
1364, 135sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
137 elpw2g 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽))
138137biimprd 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
139138ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
140136, 139mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽)
1413simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
142 unieq 4759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 = 𝑧 𝑠 = 𝑧)
143142eqeq2d 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 = 𝑧 → (𝑋 = 𝑠𝑋 = 𝑧))
144143cbvrexv 3406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)
145144imbi2i 337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
146145ralbii 3134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
147141, 146sylibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠))
148 unieq 4759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}))
149148eqeq2d 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑋 = 𝑦𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
150 breq1 4971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
151149, 150anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → ((𝑋 = 𝑦𝑦 ≼ ω) ↔ (𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)))
152 pweq 4462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
153152ineq1d 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin))
154153rexeqdv 3378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
155151, 154imbi12d 346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
156155rspccv 3558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
157147, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
158157ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
159140, 158mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
160114, 132, 159mp2and 695 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)
161 df-rex 3113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠))
162 elinel1 4099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
163 selpw 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
164 ssdif 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}))
165 difun2 4349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}) = (ran 𝑓 ∖ {(𝑋𝑎)})
166164, 165syl6sseq 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋𝑎)}))
167166difss2d 4038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
168163, 167sylbi 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
169162, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
170169a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓))
171 sseq2 3920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑋 = 𝑠 → (𝑎𝑋𝑎 𝑠))
172 uniexg 7332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐽 ∈ Top → 𝐽 ∈ V)
1731, 172syl5eqel 2889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋 ∈ V)
174 difexg 5129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑋 ∈ V → (𝑋𝑎) ∈ V)
175 unisng 4766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝑎) ∈ V → {(𝑋𝑎)} = (𝑋𝑎))
176173, 174, 1753syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽 ∈ Top → {(𝑋𝑎)} = (𝑋𝑎))
177176ineq2d 4115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = (𝑎 ∩ (𝑋𝑎)))
178 disjdif 4341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ∩ (𝑋𝑎)) = ∅
179177, 178syl6eq 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = ∅)
180 inunissunidif 34208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎 {(𝑋𝑎)}) = ∅ → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
181179, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐽 ∈ Top → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
182171, 181sylan9bbr 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
183182biimpd 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
184183impancom 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑋 = 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
185170, 184anim12d 608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
1864, 28, 185syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
187186adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
188187anim2d 611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)})))))
189118ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎 ≈ ran 𝑓)
190 fvineqsneq 34245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓 Fn 𝑎 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
19155, 190sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
192 vex 3443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑠 ∈ V
193 difss 4035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠
194 ssdomg 8410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∈ V → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠))
195192, 193, 194mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠
196191, 195syl6eqbrr 5008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → ran 𝑓𝑠)
197 endomtr 8422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓𝑠) → 𝑎𝑠)
198189, 196, 197syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎𝑠)
199188, 198syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → 𝑎𝑠))
200199expdimp 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑎𝑠))
201 elinel2 4100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ Fin)
202201adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑠 ∈ Fin)
203202a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑠 ∈ Fin))
204200, 203jcad 513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → (𝑎𝑠𝑠 ∈ Fin)))
205204eximdv 1899 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
206161, 205syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
207160, 206mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
208207ex 413 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
209208exlimdv 1915 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
210209anass1rs 651 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
2112103adant3 1125 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
21245, 211mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
21317, 26, 27, 212syl3anc 1364 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
214213anasss 467 . . . . . . . . . . . . . . . . . . 19 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
215 isfinite 8968 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ Fin ↔ 𝑠 ≺ ω)
216 domsdomtr 8506 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑠𝑠 ≺ ω) → 𝑎 ≺ ω)
217215, 216sylan2b 593 . . . . . . . . . . . . . . . . . . . 20 ((𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
218217exlimiv 1912 . . . . . . . . . . . . . . . . . . 19 (∃𝑠(𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
219 sdomnen 8393 . . . . . . . . . . . . . . . . . . 19 (𝑎 ≺ ω → ¬ 𝑎 ≈ ω)
220214, 218, 2193syl 18 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω)
22116, 220pm2.65da 813 . . . . . . . . . . . . . . . . 17 ((𝐽𝐶𝑎 ≈ ω) → ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
222 imnan 400 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
223221, 222sylibr 235 . . . . . . . . . . . . . . . 16 ((𝐽𝐶𝑎 ≈ ω) → (𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅))
224223imp 407 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅)
225 neq0 4235 . . . . . . . . . . . . . . 15 (¬ ((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
226224, 225sylib 219 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2271lpss 21438 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
2284, 227sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝐽𝐶𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
229228adantlr 711 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
230229sseld 3894 . . . . . . . . . . . . . . . . 17 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠𝑋))
231230ancrd 552 . . . . . . . . . . . . . . . 16 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
232231eximdv 1899 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
233 df-rex 3113 . . . . . . . . . . . . . . 15 (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
234232, 233syl6ibr 253 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
235226, 234mpd 15 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
23615, 235sylan2 592 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2371lpss3 21440 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑏𝑋𝑎𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2382373expb 1113 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2394, 238sylan 580 . . . . . . . . . . . . . . 15 ((𝐽𝐶 ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
240239adantlr 711 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
241240sseld 3894 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
242241reximdv 3238 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
243236, 242mpd 15 . . . . . . . . . . 11 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
244243an42s 657 . . . . . . . . . 10 (((𝐽𝐶𝑏𝑋) ∧ (𝑎𝑏𝑎 ≈ ω)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
245244ex 413 . . . . . . . . 9 ((𝐽𝐶𝑏𝑋) → ((𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
246245exlimdv 1915 . . . . . . . 8 ((𝐽𝐶𝑏𝑋) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
247246adantrr 713 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
24813, 247mpd 15 . . . . . 6 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2497, 248sylan2b 593 . . . . 5 ((𝐽𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2505, 249sylan2b 593 . . . 4 ((𝐽𝐶𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
251250ralrimiva 3151 . . 3 (𝐽𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
252 simpr 485 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → 𝑧 = 𝑠)
253 fveq2 6545 . . . . . . 7 (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
254253adantr 481 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
255252, 254eleq12d 2879 . . . . 5 ((𝑦 = 𝑏𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
256255cbvrexdva 3413 . . . 4 (𝑦 = 𝑏 → (∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
257256cbvralv 3405 . . 3 (∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
258251, 257sylibr 235 . 2 (𝐽𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))
259 pibt2.21 . . 3 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 𝑥 ∖ Fin)∃𝑧 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
2601, 259pibp21 34248 . 2 (𝐽𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))
2614, 258, 260sylanbrc 583 1 (𝐽𝐶𝐽𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1080   = wceq 1525  wex 1765  wcel 2083  wral 3107  wrex 3108  {crab 3111  Vcvv 3440  cdif 3862  cun 3863  cin 3864  wss 3865  c0 4217  𝒫 cpw 4459  {csn 4478   cuni 4751   ciun 4831   class class class wbr 4968  ran crn 5451   Fn wfn 6227  wf 6228  1-1wf1 6229  1-1-ontowf1o 6231  cfv 6232  ωcom 7443  cen 8361  cdom 8362  csdm 8363  Fincfn 8364  Topctop 21189  Clsdccld 21312  limPtclp 21430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-reg 8909  ax-inf2 8957  ax-ac2 9738
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-er 8146  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-oi 8827  df-r1 9046  df-rank 9047  df-dju 9183  df-card 9221  df-ac 9395  df-top 21190  df-cld 21315  df-ntr 21316  df-cls 21317  df-nei 21394  df-lp 21432
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator