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 37418
Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 37415 and pibp21 37416 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 37415 . . 3 (𝐽𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
43simplbi 497 . 2 (𝐽𝐶𝐽 ∈ Top)
5 eldif 3961 . . . . 5 (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin))
6 velpw 4605 . . . . . . 7 (𝑏 ∈ 𝒫 𝑋𝑏𝑋)
76anbi1i 624 . . . . . 6 ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin))
8 vex 3484 . . . . . . . . . 10 𝑏 ∈ V
9 infinf 10606 . . . . . . . . . 10 (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏))
108, 9ax-mp 5 . . . . . . . . 9 𝑏 ∈ Fin ↔ ω ≼ 𝑏)
118infcntss 9362 . . . . . . . . 9 (ω ≼ 𝑏 → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1210, 11sylbi 217 . . . . . . . 8 𝑏 ∈ Fin → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1312ad2antll 729 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
14 sstr 3992 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑏𝑋) → 𝑎𝑋)
1514ancoms 458 . . . . . . . . . . . . 13 ((𝑏𝑋𝑎𝑏) → 𝑎𝑋)
16 simplr 769 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω)
17 simpll 767 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽𝐶𝑎 ≈ ω))
18 0ss 4400 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∅ ⊆ 𝑎
19 sseq1 4009 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎))
2018, 19mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
2120adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
221cldlp 23158 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2322adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2421, 23mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
254, 24sylanl1 680 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
2625adantllr 719 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
27 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅)
281cldss 23037 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Clsd‘𝐽) → 𝑎𝑋)
291nlpineqsn 37409 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}))
30 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → (𝑛𝑎) = {𝑝})
3130reximi 3084 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∃𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∃𝑛𝐽 (𝑛𝑎) = {𝑝})
3231ralimi 3083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝})
33 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
34 ineq1 4213 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑓𝑝) → (𝑛𝑎) = ((𝑓𝑝) ∩ 𝑎))
3534eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑓𝑝) → ((𝑛𝑎) = {𝑝} ↔ ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3633, 35ac6s 10524 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
37 fvineqsnf1 37411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎1-1𝐽)
38 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})
3937, 38jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4039eximi 1835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4129, 32, 36, 404syl 19 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4228, 41syl3an2 1165 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
434, 42syl3an1 1164 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
44433adant1r 1178 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
45 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → 𝑓:𝑎1-1𝐽)
46 vsnid 4663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑝 ∈ {𝑝}
47 eleq2 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝}))
4846, 47mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓𝑝) ∩ 𝑎))
4948elin1d 4204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓𝑝))
5049ralimi 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝𝑎 𝑝 ∈ (𝑓𝑝))
51 ralssiun 37408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 𝑝 ∈ (𝑓𝑝) → 𝑎 𝑝𝑎 (𝑓𝑝))
5250, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑎 𝑝𝑎 (𝑓𝑝))
5352adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 𝑝𝑎 (𝑓𝑝))
54 f1fn 6805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:𝑎1-1𝐽𝑓 Fn 𝑎)
55 fniunfv 7267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓 Fn 𝑎 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:𝑎1-1𝐽 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5756adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5853, 57sseqtrd 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ran 𝑓)
591cldopn 23039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ (Clsd‘𝐽) → (𝑋𝑎) ∈ 𝐽)
6059ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋𝑎) ∈ 𝐽)
6160anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → ((𝑋𝑎) ∈ 𝐽𝑎 ran 𝑓))
6261ancomd 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))
6328ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎𝑋)
6463anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)))
65 unisng 4925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ∈ 𝐽 {(𝑋𝑎)} = (𝑋𝑎))
6665eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) = {(𝑋𝑎)})
67 eqimss 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) = {(𝑋𝑎)} → (𝑋𝑎) ⊆ {(𝑋𝑎)})
68 ssun4 4181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ ( ran 𝑓 {(𝑋𝑎)}))
69 uniun 4930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (ran 𝑓 ∪ {(𝑋𝑎)}) = ( ran 𝑓 {(𝑋𝑎)})
7068, 69sseqtrrdi 4025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
7166, 67, 703syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
72 ssun3 4180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑎 ran 𝑓𝑎 ⊆ ( ran 𝑓 {(𝑋𝑎)}))
7372, 69sseqtrrdi 4025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ran 𝑓𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}))
74 uncom 4158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎 ∪ (𝑋𝑎)) = ((𝑋𝑎) ∪ 𝑎)
75 undif1 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑋𝑎) ∪ 𝑎) = (𝑋𝑎)
7674, 75eqtri 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎 ∪ (𝑋𝑎)) = (𝑋𝑎)
77 ssequn2 4189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎𝑋 ↔ (𝑋𝑎) = 𝑋)
7877biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎𝑋 → (𝑋𝑎) = 𝑋)
7976, 78eqtrid 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑎𝑋 → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
8079adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
81 unss12 4188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})))
82 unidm 4157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})) = (ran 𝑓 ∪ {(𝑋𝑎)})
8381, 82sseqtrdi 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8483adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8580, 84eqsstrrd 4019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8673, 85sylanr1 682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8771, 86sylanr2 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8887adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
89 f1f 6804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎1-1𝐽𝑓:𝑎𝐽)
90 frn 6743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎𝐽 → ran 𝑓𝐽)
9189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓:𝑎1-1𝐽 → ran 𝑓𝐽)
921topopn 22912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋𝐽)
931difopn 23042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝐽𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9492, 93sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9594snssd 4809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋𝑎)} ⊆ 𝐽)
96 unss12 4188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ (𝐽𝐽))
97 unidm 4157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽𝐽) = 𝐽
9896, 97sseqtrdi 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
9991, 95, 98syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
100 uniss 4915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
101100, 1sseqtrrdi 4025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
10299, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
103102adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
10488, 103eqssd 4001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10564, 104syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10662, 105syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10758, 106sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
108107ancom1s 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
109108ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
11045, 109mpand 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
111110impr 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
112111adantlrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
1134, 112sylanl1 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
114 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑓 ∈ V
115 f1f1orn 6859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:𝑎1-1𝐽𝑓:𝑎1-1-onto→ran 𝑓)
116 f1oen3g 9007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ V ∧ 𝑓:𝑎1-1-onto→ran 𝑓) → 𝑎 ≈ ran 𝑓)
117114, 115, 116sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓:𝑎1-1𝐽𝑎 ≈ ran 𝑓)
118 enen1 9157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈ ω))
119 endom 9019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ran 𝑓 ≈ ω → ran 𝑓 ≼ ω)
120 snfi 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {(𝑋𝑎)} ∈ Fin
121 isfinite 9692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ({(𝑋𝑎)} ∈ Fin ↔ {(𝑋𝑎)} ≺ ω)
122120, 121mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {(𝑋𝑎)} ≺ ω
123 sdomdom 9020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({(𝑋𝑎)} ≺ ω → {(𝑋𝑎)} ≼ ω)
124122, 123ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {(𝑋𝑎)} ≼ ω
125 unctb 10244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ran 𝑓 ≼ ω ∧ {(𝑋𝑎)} ≼ ω) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
126119, 124, 125sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (ran 𝑓 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
127118, 126biimtrdi 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
128117, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:𝑎1-1𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
129128impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑎 ≈ ω ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
130129adantll 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
131130ad2ant2lr 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
13299ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
133132adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
134133adantlrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
1354, 134sylanl1 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
136 elpw2g 5333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽))
137136biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
138137ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
139135, 138mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽)
1403simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
141 unieq 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 = 𝑧 𝑠 = 𝑧)
142141eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 = 𝑧 → (𝑋 = 𝑠𝑋 = 𝑧))
143142cbvrexvw 3238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)
144143imbi2i 336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
145144ralbii 3093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
146140, 145sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠))
147 unieq 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}))
148147eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑋 = 𝑦𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
149 breq1 5146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
150148, 149anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → ((𝑋 = 𝑦𝑦 ≼ ω) ↔ (𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)))
151 pweq 4614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
152151ineq1d 4219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin))
153152rexeqdv 3327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
154150, 153imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
155154rspccv 3619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
156146, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
157156ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
158139, 157mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
159113, 131, 158mp2and 699 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)
160 df-rex 3071 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠))
161 elinel1 4201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
162 velpw 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
163 ssdif 4144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}))
164 difun2 4481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}) = (ran 𝑓 ∖ {(𝑋𝑎)})
165163, 164sseqtrdi 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋𝑎)}))
166165difss2d 4139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
167162, 166sylbi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
168161, 167syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
169168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓))
170 sseq2 4010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑋 = 𝑠 → (𝑎𝑋𝑎 𝑠))
171 uniexg 7760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐽 ∈ Top → 𝐽 ∈ V)
1721, 171eqeltrid 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋 ∈ V)
173 difexg 5329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑋 ∈ V → (𝑋𝑎) ∈ V)
174 unisng 4925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝑎) ∈ V → {(𝑋𝑎)} = (𝑋𝑎))
175172, 173, 1743syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽 ∈ Top → {(𝑋𝑎)} = (𝑋𝑎))
176175ineq2d 4220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = (𝑎 ∩ (𝑋𝑎)))
177 disjdif 4472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ∩ (𝑋𝑎)) = ∅
178176, 177eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = ∅)
179 inunissunidif 37376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎 {(𝑋𝑎)}) = ∅ → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
180178, 179syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐽 ∈ Top → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
181170, 180sylan9bbr 510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
182181biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
183182impancom 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑋 = 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
184169, 183anim12d 609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
1854, 28, 184syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
186185adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
187186anim2d 612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)})))))
188117ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎 ≈ ran 𝑓)
189 fvineqsneq 37413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓 Fn 𝑎 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
19054, 189sylanl1 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
191 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑠 ∈ V
192 difss 4136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠
193 ssdomg 9040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∈ V → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠))
194191, 192, 193mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠
195190, 194eqbrtrrdi 5183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → ran 𝑓𝑠)
196 endomtr 9052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓𝑠) → 𝑎𝑠)
197188, 195, 196syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎𝑠)
198187, 197syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → 𝑎𝑠))
199198expdimp 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑎𝑠))
200 elinel2 4202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ Fin)
201200adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑠 ∈ Fin)
202201a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑠 ∈ Fin))
203199, 202jcad 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → (𝑎𝑠𝑠 ∈ Fin)))
204203eximdv 1917 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
205160, 204biimtrid 242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
206159, 205mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
207206ex 412 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
208207exlimdv 1933 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
209208anass1rs 655 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
2102093adant3 1133 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
21144, 210mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
21217, 26, 27, 211syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
213212anasss 466 . . . . . . . . . . . . . . . . . . 19 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
214 isfinite 9692 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ Fin ↔ 𝑠 ≺ ω)
215 domsdomtr 9152 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑠𝑠 ≺ ω) → 𝑎 ≺ ω)
216214, 215sylan2b 594 . . . . . . . . . . . . . . . . . . . 20 ((𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
217216exlimiv 1930 . . . . . . . . . . . . . . . . . . 19 (∃𝑠(𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
218 sdomnen 9021 . . . . . . . . . . . . . . . . . . 19 (𝑎 ≺ ω → ¬ 𝑎 ≈ ω)
219213, 217, 2183syl 18 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω)
22016, 219pm2.65da 817 . . . . . . . . . . . . . . . . 17 ((𝐽𝐶𝑎 ≈ ω) → ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
221 imnan 399 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
222220, 221sylibr 234 . . . . . . . . . . . . . . . 16 ((𝐽𝐶𝑎 ≈ ω) → (𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅))
223222imp 406 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅)
224 neq0 4352 . . . . . . . . . . . . . . 15 (¬ ((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
225223, 224sylib 218 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2261lpss 23150 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
2274, 226sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝐽𝐶𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
228227adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
229228sseld 3982 . . . . . . . . . . . . . . . . 17 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠𝑋))
230229ancrd 551 . . . . . . . . . . . . . . . 16 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
231230eximdv 1917 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
232 df-rex 3071 . . . . . . . . . . . . . . 15 (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
233231, 232imbitrrdi 252 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
234225, 233mpd 15 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
23515, 234sylan2 593 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2361lpss3 23152 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑏𝑋𝑎𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2372363expb 1121 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2384, 237sylan 580 . . . . . . . . . . . . . . 15 ((𝐽𝐶 ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
239238adantlr 715 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
240239sseld 3982 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
241240reximdv 3170 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
242235, 241mpd 15 . . . . . . . . . . 11 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
243242an42s 661 . . . . . . . . . 10 (((𝐽𝐶𝑏𝑋) ∧ (𝑎𝑏𝑎 ≈ ω)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
244243ex 412 . . . . . . . . 9 ((𝐽𝐶𝑏𝑋) → ((𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
245244exlimdv 1933 . . . . . . . 8 ((𝐽𝐶𝑏𝑋) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
246245adantrr 717 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
24713, 246mpd 15 . . . . . 6 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2487, 247sylan2b 594 . . . . 5 ((𝐽𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2495, 248sylan2b 594 . . . 4 ((𝐽𝐶𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
250249ralrimiva 3146 . . 3 (𝐽𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
251 simpr 484 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → 𝑧 = 𝑠)
252 fveq2 6906 . . . . . . 7 (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
253252adantr 480 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
254251, 253eleq12d 2835 . . . . 5 ((𝑦 = 𝑏𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
255254cbvrexdva 3240 . . . 4 (𝑦 = 𝑏 → (∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
256255cbvralvw 3237 . . 3 (∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
257250, 256sylibr 234 . 2 (𝐽𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))
258 pibt2.21 . . 3 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 𝑥 ∖ Fin)∃𝑧 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
2591, 258pibp21 37416 . 2 (𝐽𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))
2604, 257, 259sylanbrc 583 1 (𝐽𝐶𝐽𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626   cuni 4907   ciun 4991   class class class wbr 5143  ran crn 5686   Fn wfn 6556  wf 6557  1-1wf1 6558  1-1-ontowf1o 6560  cfv 6561  ωcom 7887  cen 8982  cdom 8983  csdm 8984  Fincfn 8985  Topctop 22899  Clsdccld 23024  limPtclp 23142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-reg 9632  ax-inf2 9681  ax-ac2 10503
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-oi 9550  df-r1 9804  df-rank 9805  df-dju 9941  df-card 9979  df-ac 10156  df-top 22900  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator