MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnpnei Structured version   Visualization version   GIF version

Theorem cnpnei 22760
Description: A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)
Hypotheses
Ref Expression
cnpnei.1 𝑋 = βˆͺ 𝐽
cnpnei.2 π‘Œ = βˆͺ 𝐾
Assertion
Ref Expression
cnpnei (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})))
Distinct variable groups:   𝑦,𝐴   𝑦,𝐹   𝑦,𝐽   𝑦,𝐾   𝑦,𝑋   𝑦,π‘Œ

Proof of Theorem cnpnei
Dummy variables 𝑔 π‘œ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvimass 6078 . . . . . . . 8 (◑𝐹 β€œ 𝑦) βŠ† dom 𝐹
2 fdm 6724 . . . . . . . 8 (𝐹:π‘‹βŸΆπ‘Œ β†’ dom 𝐹 = 𝑋)
31, 2sseqtrid 4034 . . . . . . 7 (𝐹:π‘‹βŸΆπ‘Œ β†’ (◑𝐹 β€œ 𝑦) βŠ† 𝑋)
433ad2ant3 1136 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ (◑𝐹 β€œ 𝑦) βŠ† 𝑋)
54ad2antrr 725 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) β†’ (◑𝐹 β€œ 𝑦) βŠ† 𝑋)
6 neii2 22604 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})) β†’ βˆƒπ‘” ∈ 𝐾 ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))
763ad2antl2 1187 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})) β†’ βˆƒπ‘” ∈ 𝐾 ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))
87ad2ant2rl 748 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) β†’ βˆƒπ‘” ∈ 𝐾 ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))
9 simpll 766 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄))
10 simprl 770 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) β†’ 𝑔 ∈ 𝐾)
11 fvex 6902 . . . . . . . . . . . . . 14 (πΉβ€˜π΄) ∈ V
1211snss 4789 . . . . . . . . . . . . 13 ((πΉβ€˜π΄) ∈ 𝑔 ↔ {(πΉβ€˜π΄)} βŠ† 𝑔)
1312biimpri 227 . . . . . . . . . . . 12 ({(πΉβ€˜π΄)} βŠ† 𝑔 β†’ (πΉβ€˜π΄) ∈ 𝑔)
1413adantr 482 . . . . . . . . . . 11 (({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦) β†’ (πΉβ€˜π΄) ∈ 𝑔)
1514ad2antll 728 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) β†’ (πΉβ€˜π΄) ∈ 𝑔)
169, 10, 153jca 1129 . . . . . . . . 9 (((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑔 ∈ 𝐾 ∧ (πΉβ€˜π΄) ∈ 𝑔))
1716adantll 713 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑔 ∈ 𝐾 ∧ (πΉβ€˜π΄) ∈ 𝑔))
18 cnpimaex 22752 . . . . . . . 8 ((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑔 ∈ 𝐾 ∧ (πΉβ€˜π΄) ∈ 𝑔) β†’ βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ (𝐹 β€œ π‘œ) βŠ† 𝑔))
1917, 18syl 17 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) β†’ βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ (𝐹 β€œ π‘œ) βŠ† 𝑔))
20 sstr2 3989 . . . . . . . . . . . . 13 ((𝐹 β€œ π‘œ) βŠ† 𝑔 β†’ (𝑔 βŠ† 𝑦 β†’ (𝐹 β€œ π‘œ) βŠ† 𝑦))
2120com12 32 . . . . . . . . . . . 12 (𝑔 βŠ† 𝑦 β†’ ((𝐹 β€œ π‘œ) βŠ† 𝑔 β†’ (𝐹 β€œ π‘œ) βŠ† 𝑦))
2221ad2antll 728 . . . . . . . . . . 11 ((𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦)) β†’ ((𝐹 β€œ π‘œ) βŠ† 𝑔 β†’ (𝐹 β€œ π‘œ) βŠ† 𝑦))
2322ad2antlr 726 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) ∧ π‘œ ∈ 𝐽) β†’ ((𝐹 β€œ π‘œ) βŠ† 𝑔 β†’ (𝐹 β€œ π‘œ) βŠ† 𝑦))
24 ffun 6718 . . . . . . . . . . . . . 14 (𝐹:π‘‹βŸΆπ‘Œ β†’ Fun 𝐹)
25243ad2ant3 1136 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ Fun 𝐹)
2625ad2antrr 725 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) β†’ Fun 𝐹)
2726ad2antrr 725 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) ∧ π‘œ ∈ 𝐽) β†’ Fun 𝐹)
28 cnpnei.1 . . . . . . . . . . . . . . . . 17 𝑋 = βˆͺ 𝐽
2928eltopss 22401 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ π‘œ ∈ 𝐽) β†’ π‘œ βŠ† 𝑋)
3029adantlr 714 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘œ ∈ 𝐽) β†’ π‘œ βŠ† 𝑋)
312sseq2d 4014 . . . . . . . . . . . . . . . 16 (𝐹:π‘‹βŸΆπ‘Œ β†’ (π‘œ βŠ† dom 𝐹 ↔ π‘œ βŠ† 𝑋))
3231ad2antlr 726 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘œ ∈ 𝐽) β†’ (π‘œ βŠ† dom 𝐹 ↔ π‘œ βŠ† 𝑋))
3330, 32mpbird 257 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘œ ∈ 𝐽) β†’ π‘œ βŠ† dom 𝐹)
34333adantl2 1168 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ π‘œ ∈ 𝐽) β†’ π‘œ βŠ† dom 𝐹)
3534adantlr 714 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ π‘œ ∈ 𝐽) β†’ π‘œ βŠ† dom 𝐹)
3635ad4ant14 751 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) ∧ π‘œ ∈ 𝐽) β†’ π‘œ βŠ† dom 𝐹)
37 funimass3 7053 . . . . . . . . . . 11 ((Fun 𝐹 ∧ π‘œ βŠ† dom 𝐹) β†’ ((𝐹 β€œ π‘œ) βŠ† 𝑦 ↔ π‘œ βŠ† (◑𝐹 β€œ 𝑦)))
3827, 36, 37syl2anc 585 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) ∧ π‘œ ∈ 𝐽) β†’ ((𝐹 β€œ π‘œ) βŠ† 𝑦 ↔ π‘œ βŠ† (◑𝐹 β€œ 𝑦)))
3923, 38sylibd 238 . . . . . . . . 9 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) ∧ π‘œ ∈ 𝐽) β†’ ((𝐹 β€œ π‘œ) βŠ† 𝑔 β†’ π‘œ βŠ† (◑𝐹 β€œ 𝑦)))
4039anim2d 613 . . . . . . . 8 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) ∧ π‘œ ∈ 𝐽) β†’ ((𝐴 ∈ π‘œ ∧ (𝐹 β€œ π‘œ) βŠ† 𝑔) β†’ (𝐴 ∈ π‘œ ∧ π‘œ βŠ† (◑𝐹 β€œ 𝑦))))
4140reximdva 3169 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) β†’ (βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ (𝐹 β€œ π‘œ) βŠ† 𝑔) β†’ βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ π‘œ βŠ† (◑𝐹 β€œ 𝑦))))
4219, 41mpd 15 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) ∧ (𝑔 ∈ 𝐾 ∧ ({(πΉβ€˜π΄)} βŠ† 𝑔 ∧ 𝑔 βŠ† 𝑦))) β†’ βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ π‘œ βŠ† (◑𝐹 β€œ 𝑦)))
438, 42rexlimddv 3162 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) β†’ βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ π‘œ βŠ† (◑𝐹 β€œ 𝑦)))
4428isneip 22601 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋) β†’ ((◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) ↔ ((◑𝐹 β€œ 𝑦) βŠ† 𝑋 ∧ βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ π‘œ βŠ† (◑𝐹 β€œ 𝑦)))))
45443ad2antl1 1186 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ ((◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) ↔ ((◑𝐹 β€œ 𝑦) βŠ† 𝑋 ∧ βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ π‘œ βŠ† (◑𝐹 β€œ 𝑦)))))
4645adantr 482 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) β†’ ((◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) ↔ ((◑𝐹 β€œ 𝑦) βŠ† 𝑋 ∧ βˆƒπ‘œ ∈ 𝐽 (𝐴 ∈ π‘œ ∧ π‘œ βŠ† (◑𝐹 β€œ 𝑦)))))
475, 43, 46mpbir2and 712 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ 𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))) β†’ (◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}))
4847exp32 422 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) β†’ (𝑦 ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}) β†’ (◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}))))
4948ralrimdv 3153 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) β†’ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})))
50 simpll3 1215 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})) β†’ 𝐹:π‘‹βŸΆπ‘Œ)
51 opnneip 22615 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ π‘œ ∈ 𝐾 ∧ (πΉβ€˜π΄) ∈ π‘œ) β†’ π‘œ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}))
52 imaeq2 6054 . . . . . . . . . . . . . . . 16 (𝑦 = π‘œ β†’ (◑𝐹 β€œ 𝑦) = (◑𝐹 β€œ π‘œ))
5352eleq1d 2819 . . . . . . . . . . . . . . 15 (𝑦 = π‘œ β†’ ((◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) ↔ (◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴})))
5453rspcv 3609 . . . . . . . . . . . . . 14 (π‘œ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)}) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ (◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴})))
5551, 54syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ π‘œ ∈ 𝐾 ∧ (πΉβ€˜π΄) ∈ π‘œ) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ (◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴})))
56553com23 1127 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ (πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ (◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴})))
57563expb 1121 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ (◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴})))
58573ad2antl2 1187 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ (◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴})))
5958adantlr 714 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ (◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴})))
60 neii2 22604 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴})) β†’ βˆƒπ‘” ∈ 𝐽 ({𝐴} βŠ† 𝑔 ∧ 𝑔 βŠ† (◑𝐹 β€œ π‘œ)))
6160ex 414 . . . . . . . . . . 11 (𝐽 ∈ Top β†’ ((◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ βˆƒπ‘” ∈ 𝐽 ({𝐴} βŠ† 𝑔 ∧ 𝑔 βŠ† (◑𝐹 β€œ π‘œ))))
62613ad2ant1 1134 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ ((◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ βˆƒπ‘” ∈ 𝐽 ({𝐴} βŠ† 𝑔 ∧ 𝑔 βŠ† (◑𝐹 β€œ π‘œ))))
6362ad2antrr 725 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) β†’ ((◑𝐹 β€œ π‘œ) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ βˆƒπ‘” ∈ 𝐽 ({𝐴} βŠ† 𝑔 ∧ 𝑔 βŠ† (◑𝐹 β€œ π‘œ))))
64 snssg 4787 . . . . . . . . . . . . 13 (𝐴 ∈ 𝑋 β†’ (𝐴 ∈ 𝑔 ↔ {𝐴} βŠ† 𝑔))
6564ad3antlr 730 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) β†’ (𝐴 ∈ 𝑔 ↔ {𝐴} βŠ† 𝑔))
6625ad3antrrr 729 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) β†’ Fun 𝐹)
6728eltopss 22401 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑔 ∈ 𝐽) β†’ 𝑔 βŠ† 𝑋)
68673ad2antl1 1186 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝑔 ∈ 𝐽) β†’ 𝑔 βŠ† 𝑋)
692sseq2d 4014 . . . . . . . . . . . . . . . . 17 (𝐹:π‘‹βŸΆπ‘Œ β†’ (𝑔 βŠ† dom 𝐹 ↔ 𝑔 βŠ† 𝑋))
70693ad2ant3 1136 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ (𝑔 βŠ† dom 𝐹 ↔ 𝑔 βŠ† 𝑋))
7170biimpar 479 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝑔 βŠ† 𝑋) β†’ 𝑔 βŠ† dom 𝐹)
7268, 71syldan 592 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝑔 ∈ 𝐽) β†’ 𝑔 βŠ† dom 𝐹)
7372ad4ant14 751 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) β†’ 𝑔 βŠ† dom 𝐹)
74 funimass3 7053 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ 𝑔 βŠ† dom 𝐹) β†’ ((𝐹 β€œ 𝑔) βŠ† π‘œ ↔ 𝑔 βŠ† (◑𝐹 β€œ π‘œ)))
7566, 73, 74syl2anc 585 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) β†’ ((𝐹 β€œ 𝑔) βŠ† π‘œ ↔ 𝑔 βŠ† (◑𝐹 β€œ π‘œ)))
7665, 75anbi12d 632 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) β†’ ((𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ) ↔ ({𝐴} βŠ† 𝑔 ∧ 𝑔 βŠ† (◑𝐹 β€œ π‘œ))))
7776biimprd 247 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) ∧ 𝑔 ∈ 𝐽) β†’ (({𝐴} βŠ† 𝑔 ∧ 𝑔 βŠ† (◑𝐹 β€œ π‘œ)) β†’ (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))
7877reximdva 3169 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) β†’ (βˆƒπ‘” ∈ 𝐽 ({𝐴} βŠ† 𝑔 ∧ 𝑔 βŠ† (◑𝐹 β€œ π‘œ)) β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))
7959, 63, 783syld 60 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ ((πΉβ€˜π΄) ∈ π‘œ ∧ π‘œ ∈ 𝐾)) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))
8079exp32 422 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ ((πΉβ€˜π΄) ∈ π‘œ β†’ (π‘œ ∈ 𝐾 β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))))
8180com24 95 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ (π‘œ ∈ 𝐾 β†’ ((πΉβ€˜π΄) ∈ π‘œ β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))))
8281imp 408 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})) β†’ (π‘œ ∈ 𝐾 β†’ ((πΉβ€˜π΄) ∈ π‘œ β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ))))
8382ralrimiv 3146 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})) β†’ βˆ€π‘œ ∈ 𝐾 ((πΉβ€˜π΄) ∈ π‘œ β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))
84 cnpnei.2 . . . . . . . . 9 π‘Œ = βˆͺ 𝐾
8528, 84iscnp2 22735 . . . . . . . 8 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) ∧ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘œ ∈ 𝐾 ((πΉβ€˜π΄) ∈ π‘œ β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))))
8685baib 537 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘œ ∈ 𝐾 ((πΉβ€˜π΄) ∈ π‘œ β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))))
87863expa 1119 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘œ ∈ 𝐾 ((πΉβ€˜π΄) ∈ π‘œ β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))))
88873adantl3 1169 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘œ ∈ 𝐾 ((πΉβ€˜π΄) ∈ π‘œ β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))))
8988adantr 482 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘œ ∈ 𝐾 ((πΉβ€˜π΄) ∈ π‘œ β†’ βˆƒπ‘” ∈ 𝐽 (𝐴 ∈ 𝑔 ∧ (𝐹 β€œ 𝑔) βŠ† π‘œ)))))
9050, 83, 89mpbir2and 712 . . 3 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄))
9190ex 414 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ (βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴}) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)))
9249, 91impbid 211 1 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071   βŠ† wss 3948  {csn 4628  βˆͺ cuni 4908  β—‘ccnv 5675  dom cdm 5676   β€œ cima 5679  Fun wfun 6535  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406  Topctop 22387  neicnei 22593   CnP ccnp 22721
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 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-map 8819  df-top 22388  df-topon 22405  df-nei 22594  df-cnp 22724
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator