ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iscnp4 Unicode version
Theorem iscnp4 14386
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 14375 . . . . . 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 14182 . . . . . . . . 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 2193 . . . . . . . . . 10 |- U. K = U. K
1110neii1 14315 . . . . . . . . 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 14285 . . . . . . . 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 5694 . . . . . . . . . . . 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 14183 . . . . . . . . . . . . 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 2272 . . . . . . . . . . 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 3763 . . . . . . . . . 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 14313 . . . . . . . . . 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 5573 . . . . . . . . . 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 3752 . . . . . . . . 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 14379 . . . . . . 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 14182 . . . . . . . 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 14327 . . . . . . 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 14289 . . . . . . . . 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 3189 . . . . . 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 2598 . . . . 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 2567 . . . 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 14327 . . . . . . . . . 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 2193 . . . . . . . . . . . . . 14 |- U. J = U. J
6059neii1 14315 . . . . . . . . . . . . 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 14285 . . . . . . . . . . . 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 14183 . . . . . . . . . . . . . . . . 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 2272 . . . . . . . . . . . . . . 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 3763 . . . . . . . . . . . . . 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 14313 . . . . . . . . . . . . . 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 3752 . . . . . . . . . . . . 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 14289 . . . . . . . . . . . . . 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 5041 . . . . . . . . . . . . 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 3189 . . . . . . . . . . 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 2257 . . . . . . . . . . . . 13 |- ( z = ( ( int ` J ) ` x ) -> ( P e. z <-> P e. ( ( int ` J ) ` x ) ) )
83 imaeq2 5001 . . . . . . . . . . . . . 14 |- ( z = ( ( int ` J ) ` x ) -> ( F " z ) = ( F " ( ( int ` J ) ` x ) ) )
8483sseq1d 3208 . . . . . . . . . . . . 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 2864 . . . . . . . . . . 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 2612 . . . . . . . . 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 2564 . . . 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 14367 . . 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 2164   A.wral 2472   E.wrex 2473   _Vcvv 2760   C_ wss 3153   {csn 3618   U.cuni 3835   "cima 4662   -->wf 5250   ` cfv 5254  (class class class)co 5918   Topctop 14165  TopOnctopon 14178   intcnt 14261   neicnei 14306   CnP ccnp 14354
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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-ov 5921  df-oprab 5922  df-mpo 5923  df-1st 6193  df-2nd 6194  df-map 6704  df-top 14166  df-topon 14179  df-ntr 14264  df-nei 14307  df-cnp 14357
This theorem is referenced by:  cnnei  14400
  Copyright terms: Public domain W3C validator