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 35917
Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 35914 and pibp21 35915 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 35914 . . 3 (𝐽 ∈ 𝐢 ↔ (𝐽 ∈ Top ∧ βˆ€π‘¦ ∈ 𝒫 𝐽((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
43simplbi 499 . 2 (𝐽 ∈ 𝐢 β†’ 𝐽 ∈ Top)
5 eldif 3925 . . . . 5 (𝑏 ∈ (𝒫 𝑋 βˆ– Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ Β¬ 𝑏 ∈ Fin))
6 velpw 4570 . . . . . . 7 (𝑏 ∈ 𝒫 𝑋 ↔ 𝑏 βŠ† 𝑋)
76anbi1i 625 . . . . . 6 ((𝑏 ∈ 𝒫 𝑋 ∧ Β¬ 𝑏 ∈ Fin) ↔ (𝑏 βŠ† 𝑋 ∧ Β¬ 𝑏 ∈ Fin))
8 vex 3452 . . . . . . . . . 10 𝑏 ∈ V
9 infinf 10509 . . . . . . . . . 10 (𝑏 ∈ V β†’ (Β¬ 𝑏 ∈ Fin ↔ Ο‰ β‰Ό 𝑏))
108, 9ax-mp 5 . . . . . . . . 9 (Β¬ 𝑏 ∈ Fin ↔ Ο‰ β‰Ό 𝑏)
118infcntss 9272 . . . . . . . . 9 (Ο‰ β‰Ό 𝑏 β†’ βˆƒπ‘Ž(π‘Ž βŠ† 𝑏 ∧ π‘Ž β‰ˆ Ο‰))
1210, 11sylbi 216 . . . . . . . 8 (Β¬ 𝑏 ∈ Fin β†’ βˆƒπ‘Ž(π‘Ž βŠ† 𝑏 ∧ π‘Ž β‰ˆ Ο‰))
1312ad2antll 728 . . . . . . 7 ((𝐽 ∈ 𝐢 ∧ (𝑏 βŠ† 𝑋 ∧ Β¬ 𝑏 ∈ Fin)) β†’ βˆƒπ‘Ž(π‘Ž βŠ† 𝑏 ∧ π‘Ž β‰ˆ Ο‰))
14 sstr 3957 . . . . . . . . . . . . . 14 ((π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) β†’ π‘Ž βŠ† 𝑋)
1514ancoms 460 . . . . . . . . . . . . 13 ((𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏) β†’ π‘Ž βŠ† 𝑋)
16 simplr 768 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ (π‘Ž βŠ† 𝑋 ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…)) β†’ π‘Ž β‰ˆ Ο‰)
17 simpll 766 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ (𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰))
18 0ss 4361 . . . . . . . . . . . . . . . . . . . . . . . . . 26 βˆ… βŠ† π‘Ž
19 sseq1 3974 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((limPtβ€˜π½)β€˜π‘Ž) = βˆ… β†’ (((limPtβ€˜π½)β€˜π‘Ž) βŠ† π‘Ž ↔ βˆ… βŠ† π‘Ž))
2018, 19mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((limPtβ€˜π½)β€˜π‘Ž) = βˆ… β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† π‘Ž)
2120adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† π‘Ž)
221cldlp 22517 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋) β†’ (π‘Ž ∈ (Clsdβ€˜π½) ↔ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† π‘Ž))
2322adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ (π‘Ž ∈ (Clsdβ€˜π½) ↔ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† π‘Ž))
2421, 23mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ π‘Ž ∈ (Clsdβ€˜π½))
254, 24sylanl1 679 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ 𝐢 ∧ π‘Ž βŠ† 𝑋) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ π‘Ž ∈ (Clsdβ€˜π½))
2625adantllr 718 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ π‘Ž ∈ (Clsdβ€˜π½))
27 simpr 486 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…)
281cldss 22396 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ (Clsdβ€˜π½) β†’ π‘Ž βŠ† 𝑋)
291nlpineqsn 35908 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋 ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ βˆ€π‘ ∈ π‘Ž βˆƒπ‘› ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ π‘Ž) = {𝑝}))
30 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝 ∈ 𝑛 ∧ (𝑛 ∩ π‘Ž) = {𝑝}) β†’ (𝑛 ∩ π‘Ž) = {𝑝})
3130reximi 3088 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (βˆƒπ‘› ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ π‘Ž) = {𝑝}) β†’ βˆƒπ‘› ∈ 𝐽 (𝑛 ∩ π‘Ž) = {𝑝})
3231ralimi 3087 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆ€π‘ ∈ π‘Ž βˆƒπ‘› ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ π‘Ž) = {𝑝}) β†’ βˆ€π‘ ∈ π‘Ž βˆƒπ‘› ∈ 𝐽 (𝑛 ∩ π‘Ž) = {𝑝})
33 vex 3452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 π‘Ž ∈ V
34 ineq1 4170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (π‘“β€˜π‘) β†’ (𝑛 ∩ π‘Ž) = ((π‘“β€˜π‘) ∩ π‘Ž))
3534eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (π‘“β€˜π‘) β†’ ((𝑛 ∩ π‘Ž) = {𝑝} ↔ ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
3633, 35ac6s 10427 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (βˆ€π‘ ∈ π‘Ž βˆƒπ‘› ∈ 𝐽 (𝑛 ∩ π‘Ž) = {𝑝} β†’ βˆƒπ‘“(𝑓:π‘ŽβŸΆπ½ ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
3729, 32, 363syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋 ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ βˆƒπ‘“(𝑓:π‘ŽβŸΆπ½ ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
38 fvineqsnf1 35910 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:π‘ŽβŸΆπ½ ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ 𝑓:π‘Žβ€“1-1→𝐽)
39 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:π‘ŽβŸΆπ½ ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})
4038, 39jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:π‘ŽβŸΆπ½ ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
4140eximi 1838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆƒπ‘“(𝑓:π‘ŽβŸΆπ½ ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ βˆƒπ‘“(𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
4237, 41syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋 ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ βˆƒπ‘“(𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
4328, 42syl3an2 1165 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ βˆƒπ‘“(𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
444, 43syl3an1 1164 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽 ∈ 𝐢 ∧ π‘Ž ∈ (Clsdβ€˜π½) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ βˆƒπ‘“(𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
45443adant1r 1178 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž ∈ (Clsdβ€˜π½) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ βˆƒπ‘“(𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}))
46 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½)) ∧ 𝑓:π‘Žβ€“1-1→𝐽) β†’ 𝑓:π‘Žβ€“1-1→𝐽)
47 vsnid 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑝 ∈ {𝑝}
48 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝} β†’ (𝑝 ∈ ((π‘“β€˜π‘) ∩ π‘Ž) ↔ 𝑝 ∈ {𝑝}))
4947, 48mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝} β†’ 𝑝 ∈ ((π‘“β€˜π‘) ∩ π‘Ž))
5049elin1d 4163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝} β†’ 𝑝 ∈ (π‘“β€˜π‘))
5150ralimi 3087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝} β†’ βˆ€π‘ ∈ π‘Ž 𝑝 ∈ (π‘“β€˜π‘))
52 ralssiun 35907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (βˆ€π‘ ∈ π‘Ž 𝑝 ∈ (π‘“β€˜π‘) β†’ π‘Ž βŠ† βˆͺ 𝑝 ∈ π‘Ž (π‘“β€˜π‘))
5351, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝} β†’ π‘Ž βŠ† βˆͺ 𝑝 ∈ π‘Ž (π‘“β€˜π‘))
5453adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ π‘Ž βŠ† βˆͺ 𝑝 ∈ π‘Ž (π‘“β€˜π‘))
55 f1fn 6744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:π‘Žβ€“1-1→𝐽 β†’ 𝑓 Fn π‘Ž)
56 fniunfv 7199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓 Fn π‘Ž β†’ βˆͺ 𝑝 ∈ π‘Ž (π‘“β€˜π‘) = βˆͺ ran 𝑓)
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:π‘Žβ€“1-1→𝐽 β†’ βˆͺ 𝑝 ∈ π‘Ž (π‘“β€˜π‘) = βˆͺ ran 𝑓)
5857adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ βˆͺ 𝑝 ∈ π‘Ž (π‘“β€˜π‘) = βˆͺ ran 𝑓)
5954, 58sseqtrd 3989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ π‘Ž βŠ† βˆͺ ran 𝑓)
601cldopn 22398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (π‘Ž ∈ (Clsdβ€˜π½) β†’ (𝑋 βˆ– π‘Ž) ∈ 𝐽)
6160ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) β†’ (𝑋 βˆ– π‘Ž) ∈ 𝐽)
6261anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ π‘Ž βŠ† βˆͺ ran 𝑓) β†’ ((𝑋 βˆ– π‘Ž) ∈ 𝐽 ∧ π‘Ž βŠ† βˆͺ ran 𝑓))
6362ancomd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ π‘Ž βŠ† βˆͺ ran 𝑓) β†’ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) ∈ 𝐽))
6428ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) β†’ π‘Ž βŠ† 𝑋)
6564anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) ∈ 𝐽)) β†’ (π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) ∈ 𝐽)))
66 unisng 4891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋 βˆ– π‘Ž) ∈ 𝐽 β†’ βˆͺ {(𝑋 βˆ– π‘Ž)} = (𝑋 βˆ– π‘Ž))
6766eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋 βˆ– π‘Ž) ∈ 𝐽 β†’ (𝑋 βˆ– π‘Ž) = βˆͺ {(𝑋 βˆ– π‘Ž)})
68 eqimss 4005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋 βˆ– π‘Ž) = βˆͺ {(𝑋 βˆ– π‘Ž)} β†’ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ {(𝑋 βˆ– π‘Ž)})
69 ssun4 4140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋 βˆ– π‘Ž) βŠ† βˆͺ {(𝑋 βˆ– π‘Ž)} β†’ (𝑋 βˆ– π‘Ž) βŠ† (βˆͺ ran 𝑓 βˆͺ βˆͺ {(𝑋 βˆ– π‘Ž)}))
70 uniun 4896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) = (βˆͺ ran 𝑓 βˆͺ βˆͺ {(𝑋 βˆ– π‘Ž)})
7169, 70sseqtrrdi 4000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋 βˆ– π‘Ž) βŠ† βˆͺ {(𝑋 βˆ– π‘Ž)} β†’ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
7267, 68, 713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑋 βˆ– π‘Ž) ∈ 𝐽 β†’ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
73 ssun3 4139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (π‘Ž βŠ† βˆͺ ran 𝑓 β†’ π‘Ž βŠ† (βˆͺ ran 𝑓 βˆͺ βˆͺ {(𝑋 βˆ– π‘Ž)}))
7473, 70sseqtrrdi 4000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (π‘Ž βŠ† βˆͺ ran 𝑓 β†’ π‘Ž βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
75 uncom 4118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (π‘Ž βˆͺ (𝑋 βˆ– π‘Ž)) = ((𝑋 βˆ– π‘Ž) βˆͺ π‘Ž)
76 undif1 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑋 βˆ– π‘Ž) βˆͺ π‘Ž) = (𝑋 βˆͺ π‘Ž)
7775, 76eqtri 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (π‘Ž βˆͺ (𝑋 βˆ– π‘Ž)) = (𝑋 βˆͺ π‘Ž)
78 ssequn2 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (π‘Ž βŠ† 𝑋 ↔ (𝑋 βˆͺ π‘Ž) = 𝑋)
7978biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (π‘Ž βŠ† 𝑋 β†’ (𝑋 βˆͺ π‘Ž) = 𝑋)
8077, 79eqtrid 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (π‘Ž βŠ† 𝑋 β†’ (π‘Ž βˆͺ (𝑋 βˆ– π‘Ž)) = 𝑋)
8180adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∧ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))) β†’ (π‘Ž βˆͺ (𝑋 βˆ– π‘Ž)) = 𝑋)
82 unss12 4147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((π‘Ž βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∧ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)})) β†’ (π‘Ž βˆͺ (𝑋 βˆ– π‘Ž)) βŠ† (βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βˆͺ βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)})))
83 unidm 4117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βˆͺ βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)})) = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)})
8482, 83sseqtrdi 3999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((π‘Ž βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∧ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)})) β†’ (π‘Ž βˆͺ (𝑋 βˆ– π‘Ž)) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
8584adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∧ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))) β†’ (π‘Ž βˆͺ (𝑋 βˆ– π‘Ž)) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
8681, 85eqsstrrd 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∧ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))) β†’ 𝑋 βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
8774, 86sylanr1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))) β†’ 𝑋 βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
8872, 87sylanr2 682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) ∈ 𝐽)) β†’ 𝑋 βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
8988adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ (π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) ∈ 𝐽))) β†’ 𝑋 βŠ† βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
90 f1f 6743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:π‘Žβ€“1-1→𝐽 β†’ 𝑓:π‘ŽβŸΆπ½)
91 frn 6680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:π‘ŽβŸΆπ½ β†’ ran 𝑓 βŠ† 𝐽)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓:π‘Žβ€“1-1→𝐽 β†’ ran 𝑓 βŠ† 𝐽)
931topopn 22271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top β†’ 𝑋 ∈ 𝐽)
941difopn 22401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋 ∈ 𝐽 ∧ π‘Ž ∈ (Clsdβ€˜π½)) β†’ (𝑋 βˆ– π‘Ž) ∈ 𝐽)
9593, 94sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½)) β†’ (𝑋 βˆ– π‘Ž) ∈ 𝐽)
9695snssd 4774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½)) β†’ {(𝑋 βˆ– π‘Ž)} βŠ† 𝐽)
97 unss12 4147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((ran 𝑓 βŠ† 𝐽 ∧ {(𝑋 βˆ– π‘Ž)} βŠ† 𝐽) β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† (𝐽 βˆͺ 𝐽))
98 unidm 4117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽 βˆͺ 𝐽) = 𝐽
9997, 98sseqtrdi 3999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 βŠ† 𝐽 ∧ {(𝑋 βˆ– π‘Ž)} βŠ† 𝐽) β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝐽)
10092, 96, 99syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝐽)
101 uniss 4878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝐽 β†’ βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† βˆͺ 𝐽)
102101, 1sseqtrrdi 4000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝐽 β†’ βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝑋)
103100, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) β†’ βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝑋)
104103adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ (π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) ∈ 𝐽))) β†’ βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝑋)
10589, 104eqssd 3966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ (π‘Ž βŠ† 𝑋 ∧ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) ∈ 𝐽))) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
10665, 105syldan 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ (π‘Ž βŠ† βˆͺ ran 𝑓 ∧ (𝑋 βˆ– π‘Ž) ∈ 𝐽)) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
10763, 106syldan 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ π‘Ž βŠ† βˆͺ ran 𝑓) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
10859, 107sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ (𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½))) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
109108ancom1s 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½)) ∧ 𝑓:π‘Žβ€“1-1→𝐽) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
110109ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½)) ∧ 𝑓:π‘Žβ€“1-1→𝐽) β†’ ((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)})))
11146, 110mpand 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½)) ∧ 𝑓:π‘Žβ€“1-1→𝐽) β†’ (βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝} β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)})))
112111impr 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ Top ∧ π‘Ž ∈ (Clsdβ€˜π½)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
113112adantlrr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽 ∈ Top ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
1144, 113sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
115 vex 3452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑓 ∈ V
116 f1f1orn 6800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:π‘Žβ€“1-1→𝐽 β†’ 𝑓:π‘Žβ€“1-1-ontoβ†’ran 𝑓)
117 f1oen3g 8913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ V ∧ 𝑓:π‘Žβ€“1-1-ontoβ†’ran 𝑓) β†’ π‘Ž β‰ˆ ran 𝑓)
118115, 116, 117sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓:π‘Žβ€“1-1→𝐽 β†’ π‘Ž β‰ˆ ran 𝑓)
119 enen1 9068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘Ž β‰ˆ ran 𝑓 β†’ (π‘Ž β‰ˆ Ο‰ ↔ ran 𝑓 β‰ˆ Ο‰))
120 endom 8926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ran 𝑓 β‰ˆ Ο‰ β†’ ran 𝑓 β‰Ό Ο‰)
121 snfi 8995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {(𝑋 βˆ– π‘Ž)} ∈ Fin
122 isfinite 9595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ({(𝑋 βˆ– π‘Ž)} ∈ Fin ↔ {(𝑋 βˆ– π‘Ž)} β‰Ί Ο‰)
123121, 122mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {(𝑋 βˆ– π‘Ž)} β‰Ί Ο‰
124 sdomdom 8927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({(𝑋 βˆ– π‘Ž)} β‰Ί Ο‰ β†’ {(𝑋 βˆ– π‘Ž)} β‰Ό Ο‰)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {(𝑋 βˆ– π‘Ž)} β‰Ό Ο‰
126 unctb 10148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ran 𝑓 β‰Ό Ο‰ ∧ {(𝑋 βˆ– π‘Ž)} β‰Ό Ο‰) β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰)
127120, 125, 126sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (ran 𝑓 β‰ˆ Ο‰ β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰)
128119, 127syl6bi 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (π‘Ž β‰ˆ ran 𝑓 β†’ (π‘Ž β‰ˆ Ο‰ β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰))
129118, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:π‘Žβ€“1-1→𝐽 β†’ (π‘Ž β‰ˆ Ο‰ β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰))
130129impcom 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((π‘Ž β‰ˆ Ο‰ ∧ 𝑓:π‘Žβ€“1-1→𝐽) β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰)
131130adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰) ∧ 𝑓:π‘Žβ€“1-1→𝐽) β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰)
132131ad2ant2lr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰)
133100ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽 ∈ 𝐢 β†’ ((ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝐽))
138137biimprd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽 ∈ 𝐢 β†’ ((ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝐽 β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∈ 𝒫 𝐽))
139138ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ ((ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βŠ† 𝐽 β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∈ 𝒫 𝐽))
140136, 139mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∈ 𝒫 𝐽)
1413simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽 ∈ 𝐢 β†’ βˆ€π‘¦ ∈ 𝒫 𝐽((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧))
142 unieq 4881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 = 𝑧 β†’ βˆͺ 𝑠 = βˆͺ 𝑧)
143142eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 = 𝑧 β†’ (𝑋 = βˆͺ 𝑠 ↔ 𝑋 = βˆͺ 𝑧))
144143cbvrexvw 3229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (βˆƒπ‘  ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑠 ↔ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)
145144imbi2i 336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) β†’ βˆƒπ‘  ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑠) ↔ ((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧))
146145ralbii 3097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (βˆ€π‘¦ ∈ 𝒫 𝐽((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) β†’ βˆƒπ‘  ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑠) ↔ βˆ€π‘¦ ∈ 𝒫 𝐽((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧))
147141, 146sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽 ∈ 𝐢 β†’ βˆ€π‘¦ ∈ 𝒫 𝐽((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) β†’ βˆƒπ‘  ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑠))
148 unieq 4881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ βˆͺ 𝑦 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
149148eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ (𝑋 = βˆͺ 𝑦 ↔ 𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)})))
150 breq1 5113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ (𝑦 β‰Ό Ο‰ ↔ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰))
151149, 150anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ ((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) ↔ (𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∧ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰)))
152 pweq 4579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ 𝒫 𝑦 = 𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
153152ineq1d 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin))
154153rexeqdv 3317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ (βˆƒπ‘  ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑠 ↔ βˆƒπ‘  ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin)𝑋 = βˆͺ 𝑠))
155151, 154imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ (((𝑋 = βˆͺ 𝑦 ∧ 𝑦 β‰Ό Ο‰) β†’ βˆƒπ‘  ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑠) ↔ ((𝑋 = βˆͺ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∧ (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β‰Ό Ο‰) β†’ βˆƒπ‘  ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin)𝑋 = βˆͺ 𝑠)))
156155rspccv 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (βˆƒπ‘  ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin)𝑋 = βˆͺ 𝑠 ↔ βˆƒπ‘ (𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠))
162 elinel1 4160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) β†’ 𝑠 ∈ 𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
163 velpw 4570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ 𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ↔ 𝑠 βŠ† (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}))
164 ssdif 4104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑠 βŠ† (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ((ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βˆ– {(𝑋 βˆ– π‘Ž)}))
165 difun2 4445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) βˆ– {(𝑋 βˆ– π‘Ž)}) = (ran 𝑓 βˆ– {(𝑋 βˆ– π‘Ž)})
166164, 165sseqtrdi 3999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑠 βŠ† (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) β†’ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† (ran 𝑓 βˆ– {(𝑋 βˆ– π‘Ž)}))
167166difss2d 4099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑋 = βˆͺ 𝑠 β†’ (π‘Ž βŠ† 𝑋 ↔ π‘Ž βŠ† βˆͺ 𝑠))
172 uniexg 7682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐽 ∈ Top β†’ βˆͺ 𝐽 ∈ V)
1731, 172eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top β†’ 𝑋 ∈ V)
174 difexg 5289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑋 ∈ V β†’ (𝑋 βˆ– π‘Ž) ∈ V)
175 unisng 4891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋 βˆ– π‘Ž) ∈ V β†’ βˆͺ {(𝑋 βˆ– π‘Ž)} = (𝑋 βˆ– π‘Ž))
176173, 174, 1753syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽 ∈ Top β†’ βˆͺ {(𝑋 βˆ– π‘Ž)} = (𝑋 βˆ– π‘Ž))
177176ineq2d 4177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐽 ∈ Top β†’ (π‘Ž ∩ βˆͺ {(𝑋 βˆ– π‘Ž)}) = (π‘Ž ∩ (𝑋 βˆ– π‘Ž)))
178 disjdif 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (π‘Ž ∩ (𝑋 βˆ– π‘Ž)) = βˆ…
179177, 178eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐽 ∈ Top β†’ (π‘Ž ∩ βˆͺ {(𝑋 βˆ– π‘Ž)}) = βˆ…)
180 inunissunidif 35875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((π‘Ž ∩ βˆͺ {(𝑋 βˆ– π‘Ž)}) = βˆ… β†’ (π‘Ž βŠ† βˆͺ 𝑠 ↔ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)})))
181179, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐽 ∈ Top β†’ (π‘Ž βŠ† βˆͺ 𝑠 ↔ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)})))
182171, 181sylan9bbr 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝑠) β†’ (π‘Ž βŠ† 𝑋 ↔ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)})))
183182biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐽 ∈ Top ∧ 𝑋 = βˆͺ 𝑠) β†’ (π‘Ž βŠ† 𝑋 β†’ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)})))
184183impancom 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋) β†’ (𝑋 = βˆͺ 𝑠 β†’ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)})))
185170, 184anim12d 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋) β†’ ((𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠) β†’ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}))))
1864, 28, 185syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐽 ∈ 𝐢 ∧ π‘Ž ∈ (Clsdβ€˜π½)) β†’ ((𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠) β†’ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}))))
187186adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) β†’ ((𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠) β†’ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}))))
188187anim2d 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) β†’ (((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠)) β†’ ((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) ∧ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)})))))
189118ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) ∧ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}))) β†’ π‘Ž β‰ˆ ran 𝑓)
190 fvineqsneq 35912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓 Fn π‘Ž ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) ∧ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}))) β†’ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) = ran 𝑓)
19155, 190sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) ∧ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}))) β†’ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) = ran 𝑓)
192 vex 3452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑠 ∈ V
193 difss 4096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† 𝑠
194 ssdomg 8947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∈ V β†’ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† 𝑠 β†’ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) β‰Ό 𝑠))
195192, 193, 194mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) β‰Ό 𝑠
196191, 195eqbrtrrdi 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) ∧ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}))) β†’ ran 𝑓 β‰Ό 𝑠)
197 endomtr 8959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((π‘Ž β‰ˆ ran 𝑓 ∧ ran 𝑓 β‰Ό 𝑠) β†’ π‘Ž β‰Ό 𝑠)
198189, 196, 197syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) ∧ ((𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}) βŠ† ran 𝑓 ∧ π‘Ž βŠ† βˆͺ (𝑠 βˆ– {(𝑋 βˆ– π‘Ž)}))) β†’ π‘Ž β‰Ό 𝑠)
199188, 198syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) β†’ (((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠)) β†’ π‘Ž β‰Ό 𝑠))
200199expdimp 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ ((𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠) β†’ π‘Ž β‰Ό 𝑠))
201 elinel2 4161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) β†’ 𝑠 ∈ Fin)
202201adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠) β†’ 𝑠 ∈ Fin)
203202a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ ((𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠) β†’ 𝑠 ∈ Fin))
204200, 203jcad 514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) ∧ (𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝})) β†’ ((𝑠 ∈ (𝒫 (ran 𝑓 βˆͺ {(𝑋 βˆ– π‘Ž)}) ∩ Fin) ∧ 𝑋 = βˆͺ 𝑠) β†’ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin)))
205204eximdv 1921 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 414 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) β†’ ((𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ βˆƒπ‘ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin)))
209208exlimdv 1937 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 ∈ 𝐢 ∧ (π‘Ž ∈ (Clsdβ€˜π½) ∧ π‘Ž β‰ˆ Ο‰)) β†’ (βˆƒπ‘“(𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ βˆƒπ‘ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin)))
210209anass1rs 654 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž ∈ (Clsdβ€˜π½)) β†’ (βˆƒπ‘“(𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ βˆƒπ‘ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin)))
2112103adant3 1133 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž ∈ (Clsdβ€˜π½) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ (βˆƒπ‘“(𝑓:π‘Žβ€“1-1→𝐽 ∧ βˆ€π‘ ∈ π‘Ž ((π‘“β€˜π‘) ∩ π‘Ž) = {𝑝}) β†’ βˆƒπ‘ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin)))
21245, 211mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž ∈ (Clsdβ€˜π½) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ βˆƒπ‘ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin))
21317, 26, 27, 212syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) β†’ βˆƒπ‘ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin))
214213anasss 468 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ (π‘Ž βŠ† 𝑋 ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…)) β†’ βˆƒπ‘ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin))
215 isfinite 9595 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ Fin ↔ 𝑠 β‰Ί Ο‰)
216 domsdomtr 9063 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž β‰Ό 𝑠 ∧ 𝑠 β‰Ί Ο‰) β†’ π‘Ž β‰Ί Ο‰)
217215, 216sylan2b 595 . . . . . . . . . . . . . . . . . . . 20 ((π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin) β†’ π‘Ž β‰Ί Ο‰)
218217exlimiv 1934 . . . . . . . . . . . . . . . . . . 19 (βˆƒπ‘ (π‘Ž β‰Ό 𝑠 ∧ 𝑠 ∈ Fin) β†’ π‘Ž β‰Ί Ο‰)
219 sdomnen 8928 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β‰Ί Ο‰ β†’ Β¬ π‘Ž β‰ˆ Ο‰)
220214, 218, 2193syl 18 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ (π‘Ž βŠ† 𝑋 ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…)) β†’ Β¬ π‘Ž β‰ˆ Ο‰)
22116, 220pm2.65da 816 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) β†’ Β¬ (π‘Ž βŠ† 𝑋 ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…))
222 imnan 401 . . . . . . . . . . . . . . . . 17 ((π‘Ž βŠ† 𝑋 β†’ Β¬ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…) ↔ Β¬ (π‘Ž βŠ† 𝑋 ∧ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…))
223221, 222sylibr 233 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) β†’ (π‘Ž βŠ† 𝑋 β†’ Β¬ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…))
224223imp 408 . . . . . . . . . . . . . . 15 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) β†’ Β¬ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ…)
225 neq0 4310 . . . . . . . . . . . . . . 15 (Β¬ ((limPtβ€˜π½)β€˜π‘Ž) = βˆ… ↔ βˆƒπ‘  𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž))
226224, 225sylib 217 . . . . . . . . . . . . . 14 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) β†’ βˆƒπ‘  𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž))
2271lpss 22509 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Top ∧ π‘Ž βŠ† 𝑋) β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† 𝑋)
2284, 227sylan 581 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ 𝐢 ∧ π‘Ž βŠ† 𝑋) β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† 𝑋)
229228adantlr 714 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† 𝑋)
230229sseld 3948 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) β†’ (𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž) β†’ 𝑠 ∈ 𝑋))
231230ancrd 553 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) β†’ (𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž) β†’ (𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž))))
232231eximdv 1921 . . . . . . . . . . . . . . 15 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) β†’ (βˆƒπ‘  𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž) β†’ βˆƒπ‘ (𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž))))
233 df-rex 3075 . . . . . . . . . . . . . . 15 (βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž) ↔ βˆƒπ‘ (𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž)))
234232, 233syl6ibr 252 . . . . . . . . . . . . . 14 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) β†’ (βˆƒπ‘  𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž)))
235226, 234mpd 15 . . . . . . . . . . . . 13 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ π‘Ž βŠ† 𝑋) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž))
23615, 235sylan2 594 . . . . . . . . . . . 12 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ (𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏)) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž))
2371lpss3 22511 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏) β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† ((limPtβ€˜π½)β€˜π‘))
2382373expb 1121 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ (𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏)) β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† ((limPtβ€˜π½)β€˜π‘))
2394, 238sylan 581 . . . . . . . . . . . . . . 15 ((𝐽 ∈ 𝐢 ∧ (𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏)) β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† ((limPtβ€˜π½)β€˜π‘))
240239adantlr 714 . . . . . . . . . . . . . 14 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ (𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏)) β†’ ((limPtβ€˜π½)β€˜π‘Ž) βŠ† ((limPtβ€˜π½)β€˜π‘))
241240sseld 3948 . . . . . . . . . . . . 13 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ (𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏)) β†’ (𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž) β†’ 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘)))
242241reximdv 3168 . . . . . . . . . . . 12 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ (𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏)) β†’ (βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘Ž) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘)))
243236, 242mpd 15 . . . . . . . . . . 11 (((𝐽 ∈ 𝐢 ∧ π‘Ž β‰ˆ Ο‰) ∧ (𝑏 βŠ† 𝑋 ∧ π‘Ž βŠ† 𝑏)) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘))
244243an42s 660 . . . . . . . . . 10 (((𝐽 ∈ 𝐢 ∧ 𝑏 βŠ† 𝑋) ∧ (π‘Ž βŠ† 𝑏 ∧ π‘Ž β‰ˆ Ο‰)) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘))
245244ex 414 . . . . . . . . 9 ((𝐽 ∈ 𝐢 ∧ 𝑏 βŠ† 𝑋) β†’ ((π‘Ž βŠ† 𝑏 ∧ π‘Ž β‰ˆ Ο‰) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘)))
246245exlimdv 1937 . . . . . . . 8 ((𝐽 ∈ 𝐢 ∧ 𝑏 βŠ† 𝑋) β†’ (βˆƒπ‘Ž(π‘Ž βŠ† 𝑏 ∧ π‘Ž β‰ˆ Ο‰) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘)))
247246adantrr 716 . . . . . . 7 ((𝐽 ∈ 𝐢 ∧ (𝑏 βŠ† 𝑋 ∧ Β¬ 𝑏 ∈ Fin)) β†’ (βˆƒπ‘Ž(π‘Ž βŠ† 𝑏 ∧ π‘Ž β‰ˆ Ο‰) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘)))
24813, 247mpd 15 . . . . . 6 ((𝐽 ∈ 𝐢 ∧ (𝑏 βŠ† 𝑋 ∧ Β¬ 𝑏 ∈ Fin)) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘))
2497, 248sylan2b 595 . . . . 5 ((𝐽 ∈ 𝐢 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ Β¬ 𝑏 ∈ Fin)) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘))
2505, 249sylan2b 595 . . . 4 ((𝐽 ∈ 𝐢 ∧ 𝑏 ∈ (𝒫 𝑋 βˆ– Fin)) β†’ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘))
251250ralrimiva 3144 . . 3 (𝐽 ∈ 𝐢 β†’ βˆ€π‘ ∈ (𝒫 𝑋 βˆ– Fin)βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘))
252 simpr 486 . . . . . 6 ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) β†’ 𝑧 = 𝑠)
253 fveq2 6847 . . . . . . 7 (𝑦 = 𝑏 β†’ ((limPtβ€˜π½)β€˜π‘¦) = ((limPtβ€˜π½)β€˜π‘))
254253adantr 482 . . . . . 6 ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) β†’ ((limPtβ€˜π½)β€˜π‘¦) = ((limPtβ€˜π½)β€˜π‘))
255252, 254eleq12d 2832 . . . . 5 ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) β†’ (𝑧 ∈ ((limPtβ€˜π½)β€˜π‘¦) ↔ 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘)))
256255cbvrexdva 3330 . . . 4 (𝑦 = 𝑏 β†’ (βˆƒπ‘§ ∈ 𝑋 𝑧 ∈ ((limPtβ€˜π½)β€˜π‘¦) ↔ βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘)))
257256cbvralvw 3228 . . 3 (βˆ€π‘¦ ∈ (𝒫 𝑋 βˆ– Fin)βˆƒπ‘§ ∈ 𝑋 𝑧 ∈ ((limPtβ€˜π½)β€˜π‘¦) ↔ βˆ€π‘ ∈ (𝒫 𝑋 βˆ– Fin)βˆƒπ‘  ∈ 𝑋 𝑠 ∈ ((limPtβ€˜π½)β€˜π‘))
258251, 257sylibr 233 . 2 (𝐽 ∈ 𝐢 β†’ βˆ€π‘¦ ∈ (𝒫 𝑋 βˆ– Fin)βˆƒπ‘§ ∈ 𝑋 𝑧 ∈ ((limPtβ€˜π½)β€˜π‘¦))
259 pibt2.21 . . 3 π‘Š = {π‘₯ ∈ Top ∣ βˆ€π‘¦ ∈ (𝒫 βˆͺ π‘₯ βˆ– Fin)βˆƒπ‘§ ∈ βˆͺ π‘₯𝑧 ∈ ((limPtβ€˜π‘₯)β€˜π‘¦)}
2601, 259pibp21 35915 . 2 (𝐽 ∈ π‘Š ↔ (𝐽 ∈ Top ∧ βˆ€π‘¦ ∈ (𝒫 𝑋 βˆ– Fin)βˆƒπ‘§ ∈ 𝑋 𝑧 ∈ ((limPtβ€˜π½)β€˜π‘¦)))
2614, 258, 260sylanbrc 584 1 (𝐽 ∈ 𝐢 β†’ 𝐽 ∈ π‘Š)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3065  βˆƒwrex 3074  {crab 3410  Vcvv 3448   βˆ– cdif 3912   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  π’« cpw 4565  {csn 4591  βˆͺ cuni 4870  βˆͺ ciun 4959   class class class wbr 5110  ran crn 5639   Fn wfn 6496  βŸΆwf 6497  β€“1-1β†’wf1 6498  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501  Ο‰com 7807   β‰ˆ cen 8887   β‰Ό cdom 8888   β‰Ί csdm 8889  Fincfn 8890  Topctop 22258  Clsdccld 22383  limPtclp 22501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-reg 9535  ax-inf2 9584  ax-ac2 10406
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-oi 9453  df-r1 9707  df-rank 9708  df-dju 9844  df-card 9882  df-ac 10059  df-top 22259  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator