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 35665
Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 35662 and pibp21 35663 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 35662 . . 3 (𝐽𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
43simplbi 498 . 2 (𝐽𝐶𝐽 ∈ Top)
5 eldif 3906 . . . . 5 (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin))
6 velpw 4549 . . . . . . 7 (𝑏 ∈ 𝒫 𝑋𝑏𝑋)
76anbi1i 624 . . . . . 6 ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin))
8 vex 3444 . . . . . . . . . 10 𝑏 ∈ V
9 infinf 10401 . . . . . . . . . 10 (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏))
108, 9ax-mp 5 . . . . . . . . 9 𝑏 ∈ Fin ↔ ω ≼ 𝑏)
118infcntss 9164 . . . . . . . . 9 (ω ≼ 𝑏 → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1210, 11sylbi 216 . . . . . . . 8 𝑏 ∈ Fin → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1312ad2antll 726 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
14 sstr 3938 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑏𝑋) → 𝑎𝑋)
1514ancoms 459 . . . . . . . . . . . . 13 ((𝑏𝑋𝑎𝑏) → 𝑎𝑋)
16 simplr 766 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω)
17 simpll 764 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽𝐶𝑎 ≈ ω))
18 0ss 4340 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∅ ⊆ 𝑎
19 sseq1 3955 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎))
2018, 19mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
2120adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
221cldlp 22381 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2322adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2421, 23mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
254, 24sylanl1 677 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
2625adantllr 716 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
27 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅)
281cldss 22260 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Clsd‘𝐽) → 𝑎𝑋)
291nlpineqsn 35656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}))
30 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → (𝑛𝑎) = {𝑝})
3130reximi 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∃𝑛𝐽 (𝑛𝑎) = {𝑝})
3231ralimi 3082 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝})
33 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑎 ∈ V
34 ineq1 4149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑓𝑝) → (𝑛𝑎) = ((𝑓𝑝) ∩ 𝑎))
3534eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑓𝑝) → ((𝑛𝑎) = {𝑝} ↔ ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3633, 35ac6s 10319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3729, 32, 363syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
38 fvineqsnf1 35658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎1-1𝐽)
39 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})
4038, 39jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4140eximi 1836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4237, 41syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4328, 42syl3an2 1163 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
444, 43syl3an1 1162 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
45443adant1r 1176 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
46 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → 𝑓:𝑎1-1𝐽)
47 vsnid 4607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑝 ∈ {𝑝}
48 eleq2 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝}))
4947, 48mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓𝑝) ∩ 𝑎))
5049elin1d 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓𝑝))
5150ralimi 3082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝𝑎 𝑝 ∈ (𝑓𝑝))
52 ralssiun 35655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 𝑝 ∈ (𝑓𝑝) → 𝑎 𝑝𝑎 (𝑓𝑝))
5351, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑎 𝑝𝑎 (𝑓𝑝))
5453adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 𝑝𝑎 (𝑓𝑝))
55 f1fn 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:𝑎1-1𝐽𝑓 Fn 𝑎)
56 fniunfv 7159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓 Fn 𝑎 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:𝑎1-1𝐽 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5857adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5954, 58sseqtrd 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ran 𝑓)
601cldopn 22262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ (Clsd‘𝐽) → (𝑋𝑎) ∈ 𝐽)
6160ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋𝑎) ∈ 𝐽)
6261anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → ((𝑋𝑎) ∈ 𝐽𝑎 ran 𝑓))
6362ancomd 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))
6428ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎𝑋)
6564anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)))
66 unisng 4870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ∈ 𝐽 {(𝑋𝑎)} = (𝑋𝑎))
6766eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) = {(𝑋𝑎)})
68 eqimss 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) = {(𝑋𝑎)} → (𝑋𝑎) ⊆ {(𝑋𝑎)})
69 ssun4 4119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ ( ran 𝑓 {(𝑋𝑎)}))
70 uniun 4875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (ran 𝑓 ∪ {(𝑋𝑎)}) = ( ran 𝑓 {(𝑋𝑎)})
7169, 70sseqtrrdi 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
7267, 68, 713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
73 ssun3 4118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑎 ran 𝑓𝑎 ⊆ ( ran 𝑓 {(𝑋𝑎)}))
7473, 70sseqtrrdi 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ran 𝑓𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}))
75 uncom 4097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎 ∪ (𝑋𝑎)) = ((𝑋𝑎) ∪ 𝑎)
76 undif1 4419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑋𝑎) ∪ 𝑎) = (𝑋𝑎)
7775, 76eqtri 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎 ∪ (𝑋𝑎)) = (𝑋𝑎)
78 ssequn2 4127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎𝑋 ↔ (𝑋𝑎) = 𝑋)
7978biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎𝑋 → (𝑋𝑎) = 𝑋)
8077, 79eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑎𝑋 → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
8180adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
82 unss12 4126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})))
83 unidm 4096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})) = (ran 𝑓 ∪ {(𝑋𝑎)})
8482, 83sseqtrdi 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8584adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8681, 85eqsstrrd 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8774, 86sylanr1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8872, 87sylanr2 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8988adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
90 f1f 6707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎1-1𝐽𝑓:𝑎𝐽)
91 frn 6644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎𝐽 → ran 𝑓𝐽)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓:𝑎1-1𝐽 → ran 𝑓𝐽)
931topopn 22135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋𝐽)
941difopn 22265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝐽𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9593, 94sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9695snssd 4753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋𝑎)} ⊆ 𝐽)
97 unss12 4126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ (𝐽𝐽))
98 unidm 4096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽𝐽) = 𝐽
9997, 98sseqtrdi 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
10092, 96, 99syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
101 uniss 4857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
102101, 1sseqtrrdi 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
103100, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
104103adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
10589, 104eqssd 3947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
109108ancom1s 650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
110109ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
11146, 110mpand 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
112111impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
113112adantlrr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
1144, 113sylanl1 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
115 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑓 ∈ V
116 f1f1orn 6764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:𝑎1-1𝐽𝑓:𝑎1-1-onto→ran 𝑓)
117 f1oen3g 8805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ V ∧ 𝑓:𝑎1-1-onto→ran 𝑓) → 𝑎 ≈ ran 𝑓)
118115, 116, 117sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓:𝑎1-1𝐽𝑎 ≈ ran 𝑓)
119 enen1 8960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈ ω))
120 endom 8818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ran 𝑓 ≈ ω → ran 𝑓 ≼ ω)
121 snfi 8887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {(𝑋𝑎)} ∈ Fin
122 isfinite 9487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ({(𝑋𝑎)} ∈ Fin ↔ {(𝑋𝑎)} ≺ ω)
123121, 122mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {(𝑋𝑎)} ≺ ω
124 sdomdom 8819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({(𝑋𝑎)} ≺ ω → {(𝑋𝑎)} ≼ ω)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {(𝑋𝑎)} ≼ ω
126 unctb 10040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ran 𝑓 ≼ ω ∧ {(𝑋𝑎)} ≼ ω) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
127120, 125, 126sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (ran 𝑓 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
128119, 127syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
129118, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:𝑎1-1𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
130129impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑎 ≈ ω ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
131130adantll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
132131ad2ant2lr 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
133100ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
134133adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
135134adantlrr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
1364, 135sylanl1 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
137 elpw2g 5282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽))
138137biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
139138ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
140136, 139mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽)
1413simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
142 unieq 4860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 = 𝑧 𝑠 = 𝑧)
143142eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 = 𝑧 → (𝑋 = 𝑠𝑋 = 𝑧))
144143cbvrexvw 3222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)
145144imbi2i 335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
146145ralbii 3092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
147141, 146sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠))
148 unieq 4860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}))
149148eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑋 = 𝑦𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
150 breq1 5089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
151149, 150anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → ((𝑋 = 𝑦𝑦 ≼ ω) ↔ (𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)))
152 pweq 4558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
153152ineq1d 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin))
154153rexeqdv 3310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
155151, 154imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
156155rspccv 3566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
157147, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
158157ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
159140, 158mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
160114, 132, 159mp2and 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)
161 df-rex 3071 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠))
162 elinel1 4139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
163 velpw 4549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
164 ssdif 4084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}))
165 difun2 4424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}) = (ran 𝑓 ∖ {(𝑋𝑎)})
166164, 165sseqtrdi 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋𝑎)}))
167166difss2d 4079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
168163, 167sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
169162, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
170169a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓))
171 sseq2 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑋 = 𝑠 → (𝑎𝑋𝑎 𝑠))
172 uniexg 7634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐽 ∈ Top → 𝐽 ∈ V)
1731, 172eqeltrid 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋 ∈ V)
174 difexg 5265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑋 ∈ V → (𝑋𝑎) ∈ V)
175 unisng 4870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝑎) ∈ V → {(𝑋𝑎)} = (𝑋𝑎))
176173, 174, 1753syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽 ∈ Top → {(𝑋𝑎)} = (𝑋𝑎))
177176ineq2d 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = (𝑎 ∩ (𝑋𝑎)))
178 disjdif 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ∩ (𝑋𝑎)) = ∅
179177, 178eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = ∅)
180 inunissunidif 35623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎 {(𝑋𝑎)}) = ∅ → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
181179, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐽 ∈ Top → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
182171, 181sylan9bbr 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
183182biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
184183impancom 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑋 = 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
185170, 184anim12d 609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
1864, 28, 185syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
187186adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
188187anim2d 612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)})))))
189118ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎 ≈ ran 𝑓)
190 fvineqsneq 35660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓 Fn 𝑎 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
19155, 190sylanl1 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
192 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑠 ∈ V
193 difss 4076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠
194 ssdomg 8839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∈ V → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠))
195192, 193, 194mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠
196191, 195eqbrtrrdi 5126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → ran 𝑓𝑠)
197 endomtr 8851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1919 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
206161, 205biimtrid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
207160, 206mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
208207ex 413 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
209208exlimdv 1935 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
210209anass1rs 652 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
2112103adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
21245, 211mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
21317, 26, 27, 212syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
214213anasss 467 . . . . . . . . . . . . . . . . . . 19 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
215 isfinite 9487 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ Fin ↔ 𝑠 ≺ ω)
216 domsdomtr 8955 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑠𝑠 ≺ ω) → 𝑎 ≺ ω)
217215, 216sylan2b 594 . . . . . . . . . . . . . . . . . . . 20 ((𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
218217exlimiv 1932 . . . . . . . . . . . . . . . . . . 19 (∃𝑠(𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
219 sdomnen 8820 . . . . . . . . . . . . . . . . . . 19 (𝑎 ≺ ω → ¬ 𝑎 ≈ ω)
220214, 218, 2193syl 18 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω)
22116, 220pm2.65da 814 . . . . . . . . . . . . . . . . 17 ((𝐽𝐶𝑎 ≈ ω) → ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
222 imnan 400 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
223221, 222sylibr 233 . . . . . . . . . . . . . . . 16 ((𝐽𝐶𝑎 ≈ ω) → (𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅))
224223imp 407 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅)
225 neq0 4289 . . . . . . . . . . . . . . 15 (¬ ((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
226224, 225sylib 217 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2271lpss 22373 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
2284, 227sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝐽𝐶𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
229228adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
230229sseld 3929 . . . . . . . . . . . . . . . . 17 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠𝑋))
231230ancrd 552 . . . . . . . . . . . . . . . 16 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
232231eximdv 1919 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
233 df-rex 3071 . . . . . . . . . . . . . . 15 (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
234232, 233syl6ibr 251 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
235226, 234mpd 15 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
23615, 235sylan2 593 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2371lpss3 22375 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑏𝑋𝑎𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2382373expb 1119 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2394, 238sylan 580 . . . . . . . . . . . . . . 15 ((𝐽𝐶 ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
240239adantlr 712 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
241240sseld 3929 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
242241reximdv 3163 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
243236, 242mpd 15 . . . . . . . . . . 11 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
244243an42s 658 . . . . . . . . . 10 (((𝐽𝐶𝑏𝑋) ∧ (𝑎𝑏𝑎 ≈ ω)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
245244ex 413 . . . . . . . . 9 ((𝐽𝐶𝑏𝑋) → ((𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
246245exlimdv 1935 . . . . . . . 8 ((𝐽𝐶𝑏𝑋) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
247246adantrr 714 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
24813, 247mpd 15 . . . . . 6 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2497, 248sylan2b 594 . . . . 5 ((𝐽𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2505, 249sylan2b 594 . . . 4 ((𝐽𝐶𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
251250ralrimiva 3139 . . 3 (𝐽𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
252 simpr 485 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → 𝑧 = 𝑠)
253 fveq2 6811 . . . . . . 7 (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
254253adantr 481 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
255252, 254eleq12d 2831 . . . . 5 ((𝑦 = 𝑏𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
256255cbvrexdva 3323 . . . 4 (𝑦 = 𝑏 → (∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
257256cbvralvw 3221 . . 3 (∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
258251, 257sylibr 233 . 2 (𝐽𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))
259 pibt2.21 . . 3 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 𝑥 ∖ Fin)∃𝑧 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
2601, 259pibp21 35663 . 2 (𝐽𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))
2614, 258, 260sylanbrc 583 1 (𝐽𝐶𝐽𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wral 3061  wrex 3070  {crab 3403  Vcvv 3440  cdif 3893  cun 3894  cin 3895  wss 3896  c0 4266  𝒫 cpw 4544  {csn 4570   cuni 4849   ciun 4936   class class class wbr 5086  ran crn 5608   Fn wfn 6460  wf 6461  1-1wf1 6462  1-1-ontowf1o 6464  cfv 6465  ωcom 7758  cen 8779  cdom 8780  csdm 8781  Fincfn 8782  Topctop 22122  Clsdccld 22247  limPtclp 22365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-reg 9427  ax-inf2 9476  ax-ac2 10298
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-int 4892  df-iun 4938  df-iin 4939  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7273  df-ov 7319  df-om 7759  df-1st 7877  df-2nd 7878  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-1o 8345  df-2o 8346  df-er 8547  df-en 8783  df-dom 8784  df-sdom 8785  df-fin 8786  df-oi 9345  df-r1 9599  df-rank 9600  df-dju 9736  df-card 9774  df-ac 9951  df-top 22123  df-cld 22250  df-ntr 22251  df-cls 22252  df-nei 22329  df-lp 22367
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator