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

Theorem pibt2 34853
 Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 34850 and pibp21 34851 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 34850 . . 3 (𝐽𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
43simplbi 501 . 2 (𝐽𝐶𝐽 ∈ Top)
5 eldif 3891 . . . . 5 (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin))
6 velpw 4502 . . . . . . 7 (𝑏 ∈ 𝒫 𝑋𝑏𝑋)
76anbi1i 626 . . . . . 6 ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin))
8 vex 3444 . . . . . . . . . 10 𝑏 ∈ V
9 infinf 9980 . . . . . . . . . 10 (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏))
108, 9ax-mp 5 . . . . . . . . 9 𝑏 ∈ Fin ↔ ω ≼ 𝑏)
118infcntss 8779 . . . . . . . . 9 (ω ≼ 𝑏 → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1210, 11sylbi 220 . . . . . . . 8 𝑏 ∈ Fin → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1312ad2antll 728 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
14 sstr 3923 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑏𝑋) → 𝑎𝑋)
1514ancoms 462 . . . . . . . . . . . . 13 ((𝑏𝑋𝑎𝑏) → 𝑎𝑋)
16 simplr 768 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω)
17 simpll 766 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽𝐶𝑎 ≈ ω))
18 0ss 4304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∅ ⊆ 𝑎
19 sseq1 3940 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎))
2018, 19mpbiri 261 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
2120adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
221cldlp 21765 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2322adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2421, 23mpbird 260 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
254, 24sylanl1 679 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
2625adantllr 718 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
27 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅)
281cldss 21644 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Clsd‘𝐽) → 𝑎𝑋)
291nlpineqsn 34844 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}))
30 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → (𝑛𝑎) = {𝑝})
3130reximi 3206 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∃𝑛𝐽 (𝑛𝑎) = {𝑝})
3231ralimi 3128 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝})
33 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑎 ∈ V
34 ineq1 4131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑓𝑝) → (𝑛𝑎) = ((𝑓𝑝) ∩ 𝑎))
3534eqeq1d 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑓𝑝) → ((𝑛𝑎) = {𝑝} ↔ ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3633, 35ac6s 9898 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3729, 32, 363syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
38 fvineqsnf1 34846 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎1-1𝐽)
39 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})
4038, 39jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4140eximi 1836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4237, 41syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4328, 42syl3an2 1161 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
444, 43syl3an1 1160 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
45443adant1r 1174 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
46 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → 𝑓:𝑎1-1𝐽)
47 vsnid 4562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑝 ∈ {𝑝}
48 eleq2 2878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝}))
4947, 48mpbiri 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓𝑝) ∩ 𝑎))
5049elin1d 4125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓𝑝))
5150ralimi 3128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝𝑎 𝑝 ∈ (𝑓𝑝))
52 ralssiun 34843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 𝑝 ∈ (𝑓𝑝) → 𝑎 𝑝𝑎 (𝑓𝑝))
5351, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑎 𝑝𝑎 (𝑓𝑝))
5453adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 𝑝𝑎 (𝑓𝑝))
55 f1fn 6551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:𝑎1-1𝐽𝑓 Fn 𝑎)
56 fniunfv 6985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓 Fn 𝑎 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:𝑎1-1𝐽 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5857adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5954, 58sseqtrd 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ran 𝑓)
601cldopn 21646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ (Clsd‘𝐽) → (𝑋𝑎) ∈ 𝐽)
6160ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋𝑎) ∈ 𝐽)
6261anim1i 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → ((𝑋𝑎) ∈ 𝐽𝑎 ran 𝑓))
6362ancomd 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))
6428ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎𝑋)
6564anim1i 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)))
66 unisng 4820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ∈ 𝐽 {(𝑋𝑎)} = (𝑋𝑎))
6766eqcomd 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) = {(𝑋𝑎)})
68 eqimss 3971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) = {(𝑋𝑎)} → (𝑋𝑎) ⊆ {(𝑋𝑎)})
69 ssun4 4102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ ( ran 𝑓 {(𝑋𝑎)}))
70 uniun 4824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (ran 𝑓 ∪ {(𝑋𝑎)}) = ( ran 𝑓 {(𝑋𝑎)})
7169, 70sseqtrrdi 3966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
7267, 68, 713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
73 ssun3 4101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑎 ran 𝑓𝑎 ⊆ ( ran 𝑓 {(𝑋𝑎)}))
7473, 70sseqtrrdi 3966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ran 𝑓𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}))
75 uncom 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎 ∪ (𝑋𝑎)) = ((𝑋𝑎) ∪ 𝑎)
76 undif1 4382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑋𝑎) ∪ 𝑎) = (𝑋𝑎)
7775, 76eqtri 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎 ∪ (𝑋𝑎)) = (𝑋𝑎)
78 ssequn2 4110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎𝑋 ↔ (𝑋𝑎) = 𝑋)
7978biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎𝑋 → (𝑋𝑎) = 𝑋)
8077, 79syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑎𝑋 → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
8180adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
82 unss12 4109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})))
83 unidm 4079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})) = (ran 𝑓 ∪ {(𝑋𝑎)})
8482, 83sseqtrdi 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8584adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8681, 85eqsstrrd 3954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8774, 86sylanr1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8872, 87sylanr2 682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8988adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
90 f1f 6550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎1-1𝐽𝑓:𝑎𝐽)
91 frn 6494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎𝐽 → ran 𝑓𝐽)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓:𝑎1-1𝐽 → ran 𝑓𝐽)
931topopn 21521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋𝐽)
941difopn 21649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝐽𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9593, 94sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9695snssd 4702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋𝑎)} ⊆ 𝐽)
97 unss12 4109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ (𝐽𝐽))
98 unidm 4079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽𝐽) = 𝐽
9997, 98sseqtrdi 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
10092, 96, 99syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
101 uniss 4809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
102101, 1sseqtrrdi 3966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
103100, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
104103adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
10589, 104eqssd 3932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10665, 105syldan 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10763, 106syldan 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10859, 107sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
109108ancom1s 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
110109ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
11146, 110mpand 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
112111impr 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
113112adantlrr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
1144, 113sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
115 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑓 ∈ V
116 f1f1orn 6602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:𝑎1-1𝐽𝑓:𝑎1-1-onto→ran 𝑓)
117 f1oen3g 8511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ V ∧ 𝑓:𝑎1-1-onto→ran 𝑓) → 𝑎 ≈ ran 𝑓)
118115, 116, 117sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓:𝑎1-1𝐽𝑎 ≈ ran 𝑓)
119 enen1 8644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈ ω))
120 endom 8522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ran 𝑓 ≈ ω → ran 𝑓 ≼ ω)
121 snfi 8580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {(𝑋𝑎)} ∈ Fin
122 isfinite 9102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ({(𝑋𝑎)} ∈ Fin ↔ {(𝑋𝑎)} ≺ ω)
123121, 122mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {(𝑋𝑎)} ≺ ω
124 sdomdom 8523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({(𝑋𝑎)} ≺ ω → {(𝑋𝑎)} ≼ ω)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {(𝑋𝑎)} ≼ ω
126 unctb 9619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ran 𝑓 ≼ ω ∧ {(𝑋𝑎)} ≼ ω) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
127120, 125, 126sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (ran 𝑓 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
128119, 127syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
129118, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:𝑎1-1𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
130129impcom 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑎 ≈ ω ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
131130adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
132131ad2ant2lr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
133100ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
134133adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
135134adantlrr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
1364, 135sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
137 elpw2g 5212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽))
138137biimprd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
139138ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
140136, 139mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽)
1413simprbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
142 unieq 4812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 = 𝑧 𝑠 = 𝑧)
143142eqeq2d 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 = 𝑧 → (𝑋 = 𝑠𝑋 = 𝑧))
144143cbvrexvw 3397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)
145144imbi2i 339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
146145ralbii 3133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
147141, 146sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠))
148 unieq 4812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}))
149148eqeq2d 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑋 = 𝑦𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
150 breq1 5034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
151149, 150anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → ((𝑋 = 𝑦𝑦 ≼ ω) ↔ (𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)))
152 pweq 4513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
153152ineq1d 4138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin))
154153rexeqdv 3365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
155151, 154imbi12d 348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
156155rspccv 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
157147, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
158157ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
159140, 158mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
160114, 132, 159mp2and 698 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)
161 df-rex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠))
162 elinel1 4122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
163 velpw 4502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
164 ssdif 4067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}))
165 difun2 4387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}) = (ran 𝑓 ∖ {(𝑋𝑎)})
166164, 165sseqtrdi 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋𝑎)}))
167166difss2d 4062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
168163, 167sylbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
169162, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
170169a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓))
171 sseq2 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑋 = 𝑠 → (𝑎𝑋𝑎 𝑠))
172 uniexg 7449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐽 ∈ Top → 𝐽 ∈ V)
1731, 172eqeltrid 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋 ∈ V)
174 difexg 5196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑋 ∈ V → (𝑋𝑎) ∈ V)
175 unisng 4820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝑎) ∈ V → {(𝑋𝑎)} = (𝑋𝑎))
176173, 174, 1753syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽 ∈ Top → {(𝑋𝑎)} = (𝑋𝑎))
177176ineq2d 4139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = (𝑎 ∩ (𝑋𝑎)))
178 disjdif 4379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ∩ (𝑋𝑎)) = ∅
179177, 178eqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = ∅)
180 inunissunidif 34811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎 {(𝑋𝑎)}) = ∅ → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
181179, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐽 ∈ Top → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
182171, 181sylan9bbr 514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
183182biimpd 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
184183impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑋 = 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
185170, 184anim12d 611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
1864, 28, 185syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
187186adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
188187anim2d 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)})))))
189118ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎 ≈ ran 𝑓)
190 fvineqsneq 34848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓 Fn 𝑎 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
19155, 190sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
192 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑠 ∈ V
193 difss 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠
194 ssdomg 8541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∈ V → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠))
195192, 193, 194mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠
196191, 195eqbrtrrdi 5071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → ran 𝑓𝑠)
197 endomtr 8553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓𝑠) → 𝑎𝑠)
198189, 196, 197syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎𝑠)
199188, 198syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → 𝑎𝑠))
200199expdimp 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑎𝑠))
201 elinel2 4123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ Fin)
202201adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑠 ∈ Fin)
203202a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑠 ∈ Fin))
204200, 203jcad 516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → (𝑎𝑠𝑠 ∈ Fin)))
205204eximdv 1918 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
206161, 205syl5bi 245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
207160, 206mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
208207ex 416 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
209208exlimdv 1934 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
210209anass1rs 654 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
2112103adant3 1129 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
21245, 211mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
21317, 26, 27, 212syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
214213anasss 470 . . . . . . . . . . . . . . . . . . 19 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
215 isfinite 9102 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ Fin ↔ 𝑠 ≺ ω)
216 domsdomtr 8639 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑠𝑠 ≺ ω) → 𝑎 ≺ ω)
217215, 216sylan2b 596 . . . . . . . . . . . . . . . . . . . 20 ((𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
218217exlimiv 1931 . . . . . . . . . . . . . . . . . . 19 (∃𝑠(𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
219 sdomnen 8524 . . . . . . . . . . . . . . . . . . 19 (𝑎 ≺ ω → ¬ 𝑎 ≈ ω)
220214, 218, 2193syl 18 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω)
22116, 220pm2.65da 816 . . . . . . . . . . . . . . . . 17 ((𝐽𝐶𝑎 ≈ ω) → ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
222 imnan 403 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
223221, 222sylibr 237 . . . . . . . . . . . . . . . 16 ((𝐽𝐶𝑎 ≈ ω) → (𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅))
224223imp 410 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅)
225 neq0 4259 . . . . . . . . . . . . . . 15 (¬ ((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
226224, 225sylib 221 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2271lpss 21757 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
2284, 227sylan 583 . . . . . . . . . . . . . . . . . . 19 ((𝐽𝐶𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
229228adantlr 714 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
230229sseld 3914 . . . . . . . . . . . . . . . . 17 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠𝑋))
231230ancrd 555 . . . . . . . . . . . . . . . 16 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
232231eximdv 1918 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
233 df-rex 3112 . . . . . . . . . . . . . . 15 (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
234232, 233syl6ibr 255 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
235226, 234mpd 15 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
23615, 235sylan2 595 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2371lpss3 21759 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑏𝑋𝑎𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2382373expb 1117 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2394, 238sylan 583 . . . . . . . . . . . . . . 15 ((𝐽𝐶 ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
240239adantlr 714 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
241240sseld 3914 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
242241reximdv 3232 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
243236, 242mpd 15 . . . . . . . . . . 11 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
244243an42s 660 . . . . . . . . . 10 (((𝐽𝐶𝑏𝑋) ∧ (𝑎𝑏𝑎 ≈ ω)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
245244ex 416 . . . . . . . . 9 ((𝐽𝐶𝑏𝑋) → ((𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
246245exlimdv 1934 . . . . . . . 8 ((𝐽𝐶𝑏𝑋) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
247246adantrr 716 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
24813, 247mpd 15 . . . . . 6 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2497, 248sylan2b 596 . . . . 5 ((𝐽𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2505, 249sylan2b 596 . . . 4 ((𝐽𝐶𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
251250ralrimiva 3149 . . 3 (𝐽𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
252 simpr 488 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → 𝑧 = 𝑠)
253 fveq2 6646 . . . . . . 7 (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
254253adantr 484 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
255252, 254eleq12d 2884 . . . . 5 ((𝑦 = 𝑏𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
256255cbvrexdva 3407 . . . 4 (𝑦 = 𝑏 → (∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
257256cbvralvw 3396 . . 3 (∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
258251, 257sylibr 237 . 2 (𝐽𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))
259 pibt2.21 . . 3 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 𝑥 ∖ Fin)∃𝑧 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
2601, 259pibp21 34851 . 2 (𝐽𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))
2614, 258, 260sylanbrc 586 1 (𝐽𝐶𝐽𝑊)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ∪ cuni 4801  ∪ ciun 4882   class class class wbr 5031  ran crn 5521   Fn wfn 6320  ⟶wf 6321  –1-1→wf1 6322  –1-1-onto→wf1o 6324  ‘cfv 6325  ωcom 7563   ≈ cen 8492   ≼ cdom 8493   ≺ csdm 8494  Fincfn 8495  Topctop 21508  Clsdccld 21631  limPtclp 21749 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 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-reg 9043  ax-inf2 9091  ax-ac2 9877 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 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-oi 8961  df-r1 9180  df-rank 9181  df-dju 9317  df-card 9355  df-ac 9530  df-top 21509  df-cld 21634  df-ntr 21635  df-cls 21636  df-nei 21713  df-lp 21751 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator