Metamath Proof Explorer

Theorem iscnp4

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)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 cnpf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
2 1 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
3 2 3adantl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
4 simplr 
 |-  ( ( ( ( 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 ) )
5 simpll2 
 |-  ( ( ( ( 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 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
7 5 6 syl 
 |-  ( ( ( ( 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 )
8 eqid 
 |-  U. K = U. K
9 8 neii1 
 |-  ( ( K e. Top /\ y e. ( ( nei ` K ) ` { ( F ` P ) } ) ) -> y C_ U. K )
10 7 9 sylancom 
 |-  ( ( ( ( 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 )
11 8 ntropn 
 |-  ( ( K e. Top /\ y C_ U. K ) -> ( ( int ` K ) ` y ) e. K )
12 7 10 11 syl2anc 
 |-  ( ( ( ( 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 )
13 simpr 
 |-  ( ( ( ( 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 ) } ) )
14 3 adantr 
 |-  ( ( ( ( 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 )
15 simpll3 
 |-  ( ( ( ( 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 )
16 14 15 ffvelrnd 
 |-  ( ( ( ( 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 )
17 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
18 5 17 syl 
 |-  ( ( ( ( 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 )
19 16 18 eleqtrd 
 |-  ( ( ( ( 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 )
20 19 snssd 
 |-  ( ( ( ( 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 )
21 8 neiint 
 |-  ( ( K e. Top /\ { ( F ` P ) } C_ U. K /\ y C_ U. K ) -> ( y e. ( ( nei ` K ) ` { ( F ` P ) } ) <-> { ( F ` P ) } C_ ( ( int ` K ) ` y ) ) )
22 7 20 10 21 syl3anc 
 |-  ( ( ( ( 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 ) ) )
23 13 22 mpbid 
 |-  ( ( ( ( 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 ) )
24 fvex 
 |-  ( F ` P ) e. _V
25 24 snss 
 |-  ( ( F ` P ) e. ( ( int ` K ) ` y ) <-> { ( F ` P ) } C_ ( ( int ` K ) ` y ) )
26 23 25 sylibr 
 |-  ( ( ( ( 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 ) )
27 cnpimaex 
 |-  ( ( 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 ) ) )
28 4 12 26 27 syl3anc 
 |-  ( ( ( ( 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 ) ) )
29 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) /\ F e. ( ( J CnP K ) ` P ) ) -> J e. ( TopOn ` X ) )
30 29 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
31 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
32 30 31 syl 
 |-  ( ( ( ( ( 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 )
33 simprl 
 |-  ( ( ( ( ( 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 )
34 simprrl 
 |-  ( ( ( ( ( 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 )
35 opnneip 
 |-  ( ( J e. Top /\ x e. J /\ P e. x ) -> x e. ( ( nei ` J ) ` { P } ) )
36 32 33 34 35 syl3anc 
 |-  ( ( ( ( ( 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 } ) )
37 simprrr 
 |-  ( ( ( ( ( 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 ) )
38 8 ntrss2 
 |-  ( ( K e. Top /\ y C_ U. K ) -> ( ( int ` K ) ` y ) C_ y )
39 7 10 38 syl2anc 
 |-  ( ( ( ( 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 )
40 39 adantr 
 |-  ( ( ( ( ( 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 )
41 37 40 sstrd 
 |-  ( ( ( ( ( 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 )
42 28 36 41 reximssdv 
 |-  ( ( ( ( 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 )
43 42 ralrimiva 
 |-  ( ( ( 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 )
44 3 43 jca 
 |-  ( ( ( 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 ) )
45 44 ex 
 |-  ( ( 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 ) ) )
46 simpll2 
 |-  ( ( ( ( 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 ) )
47 46 6 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> K e. Top )
48 simprl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> y e. K )
49 simprr 
 |-  ( ( ( ( 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 )
50 opnneip 
 |-  ( ( K e. Top /\ y e. K /\ ( F ` P ) e. y ) -> y e. ( ( nei ` K ) ` { ( F ` P ) } ) )
51 47 48 49 50 syl3anc 
 |-  ( ( ( ( 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 ) } ) )
52 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) -> J e. ( TopOn ` X ) )
53 52 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
54 53 31 syl 
 |-  ( ( ( ( ( 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 )
55 simprl 
 |-  ( ( ( ( ( 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 } ) )
56 eqid 
 |-  U. J = U. J
57 56 neii1 
 |-  ( ( J e. Top /\ x e. ( ( nei ` J ) ` { P } ) ) -> x C_ U. J )
58 54 55 57 syl2anc 
 |-  ( ( ( ( ( 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 )
59 56 ntropn 
 |-  ( ( J e. Top /\ x C_ U. J ) -> ( ( int ` J ) ` x ) e. J )
60 54 58 59 syl2anc 
 |-  ( ( ( ( ( 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 )
61 simpll3 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. K /\ ( F ` P ) e. y ) ) -> P e. X )
62 61 adantr 
 |-  ( ( ( ( ( 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 )
63 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
64 53 63 syl 
 |-  ( ( ( ( ( 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 )
65 62 64 eleqtrd 
 |-  ( ( ( ( ( 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 )
66 65 snssd 
 |-  ( ( ( ( ( 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 )
67 56 neiint 
 |-  ( ( J e. Top /\ { P } C_ U. J /\ x C_ U. J ) -> ( x e. ( ( nei ` J ) ` { P } ) <-> { P } C_ ( ( int ` J ) ` x ) ) )
68 54 66 58 67 syl3anc 
 |-  ( ( ( ( ( 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 ) ) )
69 55 68 mpbid 
 |-  ( ( ( ( ( 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 ) )
70 snssg 
 |-  ( P e. X -> ( P e. ( ( int ` J ) ` x ) <-> { P } C_ ( ( int ` J ) ` x ) ) )
71 62 70 syl 
 |-  ( ( ( ( ( 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 ) ) )
72 69 71 mpbird 
 |-  ( ( ( ( ( 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 ) )
73 56 ntrss2 
 |-  ( ( J e. Top /\ x C_ U. J ) -> ( ( int ` J ) ` x ) C_ x )
74 54 58 73 syl2anc 
 |-  ( ( ( ( ( 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 )
75 imass2 
 |-  ( ( ( int ` J ) ` x ) C_ x -> ( F " ( ( int ` J ) ` x ) ) C_ ( F " x ) )
76 74 75 syl 
 |-  ( ( ( ( ( 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 ) )
77 simprr 
 |-  ( ( ( ( ( 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 )
78 76 77 sstrd 
 |-  ( ( ( ( ( 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 )
79 eleq2 
 |-  ( z = ( ( int ` J ) ` x ) -> ( P e. z <-> P e. ( ( int ` J ) ` x ) ) )
80 imaeq2 
 |-  ( z = ( ( int ` J ) ` x ) -> ( F " z ) = ( F " ( ( int ` J ) ` x ) ) )
81 80 sseq1d 
 |-  ( z = ( ( int ` J ) ` x ) -> ( ( F " z ) C_ y <-> ( F " ( ( int ` J ) ` x ) ) C_ y ) )
82 79 81 anbi12d 
 |-  ( z = ( ( int ` J ) ` x ) -> ( ( P e. z /\ ( F " z ) C_ y ) <-> ( P e. ( ( int ` J ) ` x ) /\ ( F " ( ( int ` J ) ` x ) ) C_ y ) ) )
83 82 rspcev 
 |-  ( ( ( ( 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 ) )
84 60 72 78 83 syl12anc 
 |-  ( ( ( ( ( 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 ) )
85 84 rexlimdvaa 
 |-  ( ( ( ( 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 ) ) )
86 51 85 embantd 
 |-  ( ( ( ( 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 ) ) )
87 86 ex 
 |-  ( ( ( 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 ) ) ) )
88 87 com23 
 |-  ( ( ( 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 ) ) ) )
89 88 exp4a 
 |-  ( ( ( 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 ) ) ) ) )
90 89 ralimdv2 
 |-  ( ( ( 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 ) ) ) )
91 90 imdistanda 
 |-  ( ( 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 ) ) ) ) )
92 iscnp 
 |-  ( ( 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 ) ) ) ) )
93 91 92 sylibrd 
 |-  ( ( 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 ) ) )
94 45 93 impbid 
 |-  ( ( 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 ) ) )