ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iscnp4 Unicode version
Theorem iscnp4 14454
Description: The predicate "the class F is a continuous function from topology J to topology K at point P " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
iscnp4 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) ) )
Distinct variable groups:   x, y, F   x, J, y   x, K, y   x, P, y   x, X, y   x, Y, y
Proof of Theorem iscnp4
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 cnpf2 14443 . . . . . 6 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
213expa 1205 . . . . 5 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
323adantl3 1157 . . . 4 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
4 simpll1 1038 . . . . . . 7 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> J e. (TopOn ` X ) )
5 simpll2 1039 . . . . . . 7 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> K e. (TopOn ` Y ) )
6 simpll3 1040 . . . . . . 7 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> P e. X )
7 simplr 528 . . . . . . 7 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> F e. ( ( J CnP K ) ` P ) )
8 topontop 14250 . . . . . . . . 9 |- ( K e. (TopOn ` Y ) -> K e. Top )
95, 8syl 14 . . . . . . . 8 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> K e. Top )
10 eqid 2196 . . . . . . . . . 10 |- U. K = U. K
1110neii1 14383 . . . . . . . . 9 |- ( ( K e. Top /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> y C_ U. K )
129, 11sylancom 420 . . . . . . . 8 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> y C_ U. K )
1310ntropn 14353 . . . . . . . 8 |- ( ( K e. Top /\ y C_ U. K ) -> ( ( int ` K ) ` y ) e. K )
149, 12, 13syl2anc 411 . . . . . . 7 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> ( ( int ` K ) ` y ) e. K )
15 simpr 110 . . . . . . . . 9 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> y e. ( ( nei ` K ) ` { ( F ` P ) } ) )
163adantr 276 . . . . . . . . . . . . 13 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> F : X --> Y )
1716, 6ffvelcdmd 5698 . . . . . . . . . . . 12 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> ( F ` P ) e. Y )
18 toponuni 14251 . . . . . . . . . . . . 13 |- ( K e. (TopOn ` Y ) -> Y = U. K )
195, 18syl 14 . . . . . . . . . . . 12 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> Y = U. K )
2017, 19eleqtrd 2275 . . . . . . . . . . 11 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> ( F ` P ) e. U. K )
2120snssd 3767 . . . . . . . . . 10 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> { ( F ` P ) } C_ U. K )
2210neiint 14381 . . . . . . . . . 10 |- ( ( K e. Top /\ { ( F ` P ) } C_ U. K /\ y C_ U. K ) -> ( y e. ( ( nei ` K ) ` { ( F ` P ) } ) <-> { ( F ` P ) } C_ ( ( int ` K ) ` y ) ) )
239, 21, 12, 22syl3anc 1249 . . . . . . . . 9 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> ( y e. ( ( nei ` K ) ` { ( F ` P ) } ) <-> { ( F ` P ) } C_ ( ( int ` K ) ` y ) ) )
2415, 23mpbid 147 . . . . . . . 8 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> { ( F ` P ) } C_ ( ( int ` K ) ` y ) )
25 fvexg 5577 . . . . . . . . . 10 |- ( ( F e. ( ( J CnP K ) ` P ) /\ P e. X ) -> ( F ` P ) e. _V )
267, 6, 25syl2anc 411 . . . . . . . . 9 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> ( F ` P ) e. _V )
27 snssg 3756 . . . . . . . . 9 |- ( ( F ` P ) e. _V -> ( ( F ` P ) e. ( ( int ` K ) ` y ) <-> { ( F ` P ) } C_ ( ( int ` K ) ` y ) ) )
2826, 27syl 14 . . . . . . . 8 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> ( ( F ` P ) e. ( ( int ` K ) ` y ) <-> { ( F ` P ) } C_ ( ( int ` K ) ` y ) ) )
2924, 28mpbird 167 . . . . . . 7 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> ( F ` P ) e. ( ( int ` K ) ` y ) )
30 icnpimaex 14447 . . . . . . 7 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ ( F e. ( ( J CnP K ) ` P ) /\ ( ( int ` K ) ` y ) e. K /\ ( F ` P ) e. ( ( int ` K ) ` y ) ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) )
314, 5, 6, 7, 14, 29, 30syl33anc 1264 . . . . . 6 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) )
32 simpl1 1002 . . . . . . . . 9 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) -> J e. (TopOn ` X ) )
3332ad2antrr 488 . . . . . . . 8 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) /\ ( x e. J /\ ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) ) ) -> J e. (TopOn ` X ) )
34 topontop 14250 . . . . . . . 8 |- ( J e. (TopOn ` X ) -> J e. Top )
3533, 34syl 14 . . . . . . 7 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) /\ ( x e. J /\ ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) ) ) -> J e. Top )
36 simprl 529 . . . . . . 7 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) /\ ( x e. J /\ ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) ) ) -> x e. J )
37 simprrl 539 . . . . . . 7 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) /\ ( x e. J /\ ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) ) ) -> P e. x )
38 opnneip 14395 . . . . . . 7 |- ( ( J e. Top /\ x e. J /\ P e. x ) -> x e. ( ( nei ` J ) ` { P } ) )
3935, 36, 37, 38syl3anc 1249 . . . . . 6 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) /\ ( x e. J /\ ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) ) ) -> x e. ( ( nei ` J ) ` { P } ) )
40 simprrr 540 . . . . . . 7 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) /\ ( x e. J /\ ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) ) ) -> ( F " x ) C_ ( ( int ` K ) ` y ) )
4110ntrss2 14357 . . . . . . . . 9 |- ( ( K e. Top /\ y C_ U. K ) -> ( ( int ` K ) ` y ) C_ y )
429, 12, 41syl2anc 411 . . . . . . . 8 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> ( ( int ` K ) ` y ) C_ y )
4342adantr 276 . . . . . . 7 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) /\ ( x e. J /\ ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) ) ) -> ( ( int ` K ) ` y ) C_ y )
4440, 43sstrd 3193 . . . . . 6 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) /\ ( x e. J /\ ( P e. x /\ ( F " x ) C_ ( ( int ` K ) ` y ) ) ) ) -> ( F " x ) C_ y )
4531, 39, 44reximssdv 2601 . . . . 5 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y )
4645ralrimiva 2570 . . . 4 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) -> A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y )
473, 46jca 306 . . 3 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) -> ( F : X --> Y /\ A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) )
4847ex 115 . 2 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) -> ( F : X --> Y /\ A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) ) )
49 simpll2 1039 . . . . . . . . . . 11 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> K e. (TopOn ` Y ) )
5049, 8syl 14 . . . . . . . . . 10 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> K e. Top )
51 simprl 529 . . . . . . . . . 10 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> y e. K )
52 simprr 531 . . . . . . . . . 10 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> ( F ` P ) e. y )
53 opnneip 14395 . . . . . . . . . 10 |- ( ( K e. Top /\ y e. K /\ ( F ` P ) e. y ) -> y e. ( ( nei ` K ) ` { ( F ` P ) } ) )
5450, 51, 52, 53syl3anc 1249 . . . . . . . . 9 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> y e. ( ( nei ` K ) ` { ( F ` P ) } ) )
55 simpl1 1002 . . . . . . . . . . . . . 14 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) -> J e. (TopOn ` X ) )
5655ad2antrr 488 . . . . . . . . . . . . 13 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> J e. (TopOn ` X ) )
5756, 34syl 14 . . . . . . . . . . . 12 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> J e. Top )
58 simprl 529 . . . . . . . . . . . . 13 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> x e. ( ( nei ` J ) ` { P } ) )
59 eqid 2196 . . . . . . . . . . . . . 14 |- U. J = U. J
6059neii1 14383 . . . . . . . . . . . . 13 |- ( ( J e. Top /\ x e. ( ( nei ` J ) ` { P } ) ) -> x C_ U. J )
6157, 58, 60syl2anc 411 . . . . . . . . . . . 12 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> x C_ U. J )
6259ntropn 14353 . . . . . . . . . . . 12 |- ( ( J e. Top /\ x C_ U. J ) -> ( ( int ` J ) ` x ) e. J )
6357, 61, 62syl2anc 411 . . . . . . . . . . 11 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> ( ( int ` J ) ` x ) e. J )
64 simpll3 1040 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> P e. X )
6564adantr 276 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> P e. X )
66 toponuni 14251 . . . . . . . . . . . . . . . . 17 |- ( J e. (TopOn ` X ) -> X = U. J )
6756, 66syl 14 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> X = U. J )
6865, 67eleqtrd 2275 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> P e. U. J )
6968snssd 3767 . . . . . . . . . . . . . 14 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> { P } C_ U. J )
7059neiint 14381 . . . . . . . . . . . . . 14 |- ( ( J e. Top /\ { P } C_ U. J /\ x C_ U. J ) -> ( x e. ( ( nei ` J ) ` { P } ) <-> { P } C_ ( ( int ` J ) ` x ) ) )
7157, 69, 61, 70syl3anc 1249 . . . . . . . . . . . . 13 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> ( x e. ( ( nei ` J ) ` { P } ) <-> { P } C_ ( ( int ` J ) ` x ) ) )
7258, 71mpbid 147 . . . . . . . . . . . 12 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> { P } C_ ( ( int ` J ) ` x ) )
73 snssg 3756 . . . . . . . . . . . . 13 |- ( P e. X -> ( P e. ( ( int ` J ) ` x ) <-> { P } C_ ( ( int ` J ) ` x ) ) )
7465, 73syl 14 . . . . . . . . . . . 12 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> ( P e. ( ( int ` J ) ` x ) <-> { P } C_ ( ( int ` J ) ` x ) ) )
7572, 74mpbird 167 . . . . . . . . . . 11 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> P e. ( ( int ` J ) ` x ) )
7659ntrss2 14357 . . . . . . . . . . . . . 14 |- ( ( J e. Top /\ x C_ U. J ) -> ( ( int ` J ) ` x ) C_ x )
7757, 61, 76syl2anc 411 . . . . . . . . . . . . 13 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> ( ( int ` J ) ` x ) C_ x )
78 imass2 5045 . . . . . . . . . . . . 13 |- ( ( ( int ` J ) ` x ) C_ x -> ( F " ( ( int ` J ) ` x ) ) C_ ( F " x ) )
7977, 78syl 14 . . . . . . . . . . . 12 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> ( F " ( ( int ` J ) ` x ) ) C_ ( F " x ) )
80 simprr 531 . . . . . . . . . . . 12 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> ( F " x ) C_ y )
8179, 80sstrd 3193 . . . . . . . . . . 11 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> ( F " ( ( int ` J ) ` x ) ) C_ y )
82 eleq2 2260 . . . . . . . . . . . . 13 |- ( z = ( ( int ` J ) ` x ) -> ( P e. z <-> P e. ( ( int ` J ) ` x ) ) )
83 imaeq2 5005 . . . . . . . . . . . . . 14 |- ( z = ( ( int ` J ) ` x ) -> ( F " z ) = ( F " ( ( int ` J ) ` x ) ) )
8483sseq1d 3212 . . . . . . . . . . . . 13 |- ( z = ( ( int ` J ) ` x ) -> ( ( F " z ) C_ y <-> ( F " ( ( int ` J ) ` x ) ) C_ y ) )
8582, 84anbi12d 473 . . . . . . . . . . . 12 |- ( z = ( ( int ` J ) ` x ) -> ( ( P e. z /\ ( F " z ) C_ y ) <-> ( P e. ( ( int ` J ) ` x ) /\ ( F " ( ( int ` J ) ` x ) ) C_ y ) ) )
8685rspcev 2868 . . . . . . . . . . 11 |- ( ( ( ( int ` J ) ` x ) e. J /\ ( P e. ( ( int ` J ) ` x ) /\ ( F " ( ( int ` J ) ` x ) ) C_ y ) ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) )
8763, 75, 81, 86syl12anc 1247 . . . . . . . . . 10 |- ( ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) /\ ( x e. ( ( nei ` J ) ` { P } ) /\ ( F " x ) C_ y ) ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) )
8887rexlimdvaa 2615 . . . . . . . . 9 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> ( E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) )
8954, 88embantd 56 . . . . . . . 8 |- ( ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> ( ( y e. ( ( nei ` K ) ` { ( F ` P ) } ) -> E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) )
9089ex 115 . . . . . . 7 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( ( y e. K /\ ( F ` P ) e. y ) -> ( ( y e. ( ( nei ` K ) ` { ( F ` P ) } ) -> E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) )
9190com23 78 . . . . . 6 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( ( y e. ( ( nei ` K ) ` { ( F ` P ) } ) -> E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) -> ( ( y e. K /\ ( F ` P ) e. y ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) )
9291exp4a 366 . . . . 5 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( ( y e. ( ( nei ` K ) ` { ( F ` P ) } ) -> E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) -> ( y e. K -> ( ( F ` P ) e. y -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) ) )
9392ralimdv2 2567 . . . 4 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y -> A. y e. K ( ( F ` P ) e. y -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) )
9493imdistanda 448 . . 3 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( ( F : X --> Y /\ A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) -> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) ) )
95 iscnp 14435 . . 3 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) ) )
9694, 95sylibrd 169 . 2 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( ( F : X --> Y /\ A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) -> F e. ( ( J CnP K ) ` P ) ) )
9748, 96impbid 129 1 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) ) )
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 980   = wceq 1364   e. wcel 2167   A.wral 2475   E.wrex 2476   _Vcvv 2763   C_ wss 3157   {csn 3622   U.cuni 3839   "cima 4666   -->wf 5254   ` cfv 5258  (class class class)co 5922   Topctop 14233  TopOnctopon 14246   intcnt 14329   neicnei 14374   CnP ccnp 14422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-map 6709  df-top 14234  df-topon 14247  df-ntr 14332  df-nei 14375  df-cnp 14425
This theorem is referenced by:  cnnei  14468
  Copyright terms: Public domain W3C validator