ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iscnp4 Unicode version
Theorem iscnp4 13012
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 13001 . . . . . 6 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
213expa 1198 . . . . 5 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
323adantl3 1150 . . . 4 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
4 simpll1 1031 . . . . . . 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 1032 . . . . . . 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 1033 . . . . . . 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 525 . . . . . . 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 12806 . . . . . . . . 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 2170 . . . . . . . . . 10 |- U. K = U. K
1110neii1 12941 . . . . . . . . 9 |- ( ( K e. Top /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> y C_ U. K )
129, 11sylancom 418 . . . . . . . 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 12911 . . . . . . . 8 |- ( ( K e. Top /\ y C_ U. K ) -> ( ( int ` K ) ` y ) e. K )
149, 12, 13syl2anc 409 . . . . . . 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 109 . . . . . . . . 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 274 . . . . . . . . . . . . 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, 6ffvelrnd 5632 . . . . . . . . . . . 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 12807 . . . . . . . . . . . . 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 2249 . . . . . . . . . . 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 3725 . . . . . . . . . 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 12939 . . . . . . . . . 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 1233 . . . . . . . . 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 146 . . . . . . . 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 5515 . . . . . . . . . 10 |- ( ( F e. ( ( J CnP K ) ` P ) /\ P e. X ) -> ( F ` P ) e. _V )
267, 6, 25syl2anc 409 . . . . . . . . 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 3716 . . . . . . . . 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 166 . . . . . . 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 13005 . . . . . . 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 1248 . . . . . 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 995 . . . . . . . . 9 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) -> J e. (TopOn ` X ) )
3332ad2antrr 485 . . . . . . . 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 12806 . . . . . . . 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 526 . . . . . . 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 534 . . . . . . 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 12953 . . . . . . 7 |- ( ( J e. Top /\ x e. J /\ P e. x ) -> x e. ( ( nei ` J ) ` { P } ) )
3935, 36, 37, 38syl3anc 1233 . . . . . 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 535 . . . . . . 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 12915 . . . . . . . . 9 |- ( ( K e. Top /\ y C_ U. K ) -> ( ( int ` K ) ` y ) C_ y )
429, 12, 41syl2anc 409 . . . . . . . 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 274 . . . . . . 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 3157 . . . . . 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 2574 . . . . 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 2543 . . . 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 304 . . 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 114 . 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 1032 . . . . . . . . . . 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 526 . . . . . . . . . 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 527 . . . . . . . . . 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 12953 . . . . . . . . . 10 |- ( ( K e. Top /\ y e. K /\ ( F ` P ) e. y ) -> y e. ( ( nei ` K ) ` { ( F ` P ) } ) )
5450, 51, 52, 53syl3anc 1233 . . . . . . . . 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 995 . . . . . . . . . . . . . 14 |- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) -> J e. (TopOn ` X ) )
5655ad2antrr 485 . . . . . . . . . . . . 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 526 . . . . . . . . . . . . 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 2170 . . . . . . . . . . . . . 14 |- U. J = U. J
6059neii1 12941 . . . . . . . . . . . . 13 |- ( ( J e. Top /\ x e. ( ( nei ` J ) ` { P } ) ) -> x C_ U. J )
6157, 58, 60syl2anc 409 . . . . . . . . . . . 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 12911 . . . . . . . . . . . 12 |- ( ( J e. Top /\ x C_ U. J ) -> ( ( int ` J ) ` x ) e. J )
6357, 61, 62syl2anc 409 . . . . . . . . . . 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 1033 . . . . . . . . . . . . . . . . 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 274 . . . . . . . . . . . . . . . 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 12807 . . . . . . . . . . . . . . . . 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 2249 . . . . . . . . . . . . . . 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 3725 . . . . . . . . . . . . . 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 12939 . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . 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 146 . . . . . . . . . . . 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 3716 . . . . . . . . . . . . 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 166 . . . . . . . . . . 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 12915 . . . . . . . . . . . . . 14 |- ( ( J e. Top /\ x C_ U. J ) -> ( ( int ` J ) ` x ) C_ x )
7757, 61, 76syl2anc 409 . . . . . . . . . . . . 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 4987 . . . . . . . . . . . . 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 527 . . . . . . . . . . . 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 3157 . . . . . . . . . . 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 2234 . . . . . . . . . . . . 13 |- ( z = ( ( int ` J ) ` x ) -> ( P e. z <-> P e. ( ( int ` J ) ` x ) ) )
83 imaeq2 4949 . . . . . . . . . . . . . 14 |- ( z = ( ( int ` J ) ` x ) -> ( F " z ) = ( F " ( ( int ` J ) ` x ) ) )
8483sseq1d 3176 . . . . . . . . . . . . 13 |- ( z = ( ( int ` J ) ` x ) -> ( ( F " z ) C_ y <-> ( F " ( ( int ` J ) ` x ) ) C_ y ) )
8582, 84anbi12d 470 . . . . . . . . . . . 12 |- ( z = ( ( int ` J ) ` x ) -> ( ( P e. z /\ ( F " z ) C_ y ) <-> ( P e. ( ( int ` J ) ` x ) /\ ( F " ( ( int ` J ) ` x ) ) C_ y ) ) )
8685rspcev 2834 . . . . . . . . . . 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 1231 . . . . . . . . . 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 2588 . . . . . . . . 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 114 . . . . . . 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 364 . . . . 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 2540 . . . 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 446 . . 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 12993 . . 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 168 . 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 128 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 103   <-> wb 104   /\ w3a 973   = wceq 1348   e. wcel 2141   A.wral 2448   E.wrex 2449   _Vcvv 2730   C_ wss 3121   {csn 3583   U.cuni 3796   "cima 4614   -->wf 5194   ` cfv 5198  (class class class)co 5853   Topctop 12789  TopOnctopon 12802   intcnt 12887   neicnei 12932   CnP ccnp 12980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-map 6628  df-top 12790  df-topon 12803  df-ntr 12890  df-nei 12933  df-cnp 12983
This theorem is referenced by:  cnnei  13026
  Copyright terms: Public domain W3C validator