This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnprest

Description: Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014)

Ref Expression
Hypotheses cnprest.1 
|- X = U. J
cnprest.2 
|- Y = U. K
Assertion cnprest 
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) ) )

Proof

Step Hyp Ref Expression
1 cnprest.1 
 |-  X = U. J
2 cnprest.2 
 |-  Y = U. K
3 cnptop2 
 |-  ( F e. ( ( J CnP K ) ` P ) -> K e. Top )
4 3 a1i 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( F e. ( ( J CnP K ) ` P ) -> K e. Top ) )
5 cnptop2 
 |-  ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) -> K e. Top )
6 5 a1i 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) -> K e. Top ) )
7 1 ntrss2 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) C_ A )
8 7 3ad2ant1 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( int ` J ) ` A ) C_ A )
9 simp2l 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> P e. ( ( int ` J ) ` A ) )
10 8 9 sseldd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> P e. A )
11 10 fvresd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F |` A ) ` P ) = ( F ` P ) )
12 11 eqcomd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F ` P ) = ( ( F |` A ) ` P ) )
13 12 eleq1d 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F ` P ) e. y <-> ( ( F |` A ) ` P ) e. y ) )
14 inss1 
 |-  ( x i^i A ) C_ x
15 imass2 
 |-  ( ( x i^i A ) C_ x -> ( F " ( x i^i A ) ) C_ ( F " x ) )
16 sstr2 
 |-  ( ( F " ( x i^i A ) ) C_ ( F " x ) -> ( ( F " x ) C_ y -> ( F " ( x i^i A ) ) C_ y ) )
17 14 15 16 mp2b 
 |-  ( ( F " x ) C_ y -> ( F " ( x i^i A ) ) C_ y )
18 17 anim2i 
 |-  ( ( P e. x /\ ( F " x ) C_ y ) -> ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) )
19 18 reximi 
 |-  ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) )
20 simp1l 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> J e. Top )
21 1 ntropn 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) e. J )
22 21 3ad2ant1 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( int ` J ) ` A ) e. J )
23 inopn 
 |-  ( ( J e. Top /\ x e. J /\ ( ( int ` J ) ` A ) e. J ) -> ( x i^i ( ( int ` J ) ` A ) ) e. J )
24 23 3com23 
 |-  ( ( J e. Top /\ ( ( int ` J ) ` A ) e. J /\ x e. J ) -> ( x i^i ( ( int ` J ) ` A ) ) e. J )
25 24 3expia 
 |-  ( ( J e. Top /\ ( ( int ` J ) ` A ) e. J ) -> ( x e. J -> ( x i^i ( ( int ` J ) ` A ) ) e. J ) )
26 20 22 25 syl2anc 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( x e. J -> ( x i^i ( ( int ` J ) ` A ) ) e. J ) )
27 elin 
 |-  ( P e. ( x i^i ( ( int ` J ) ` A ) ) <-> ( P e. x /\ P e. ( ( int ` J ) ` A ) ) )
28 27 simplbi2com 
 |-  ( P e. ( ( int ` J ) ` A ) -> ( P e. x -> P e. ( x i^i ( ( int ` J ) ` A ) ) ) )
29 9 28 syl 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( P e. x -> P e. ( x i^i ( ( int ` J ) ` A ) ) ) )
30 sslin 
 |-  ( ( ( int ` J ) ` A ) C_ A -> ( x i^i ( ( int ` J ) ` A ) ) C_ ( x i^i A ) )
31 8 30 syl 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( x i^i ( ( int ` J ) ` A ) ) C_ ( x i^i A ) )
32 imass2 
 |-  ( ( x i^i ( ( int ` J ) ` A ) ) C_ ( x i^i A ) -> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ ( F " ( x i^i A ) ) )
33 31 32 syl 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ ( F " ( x i^i A ) ) )
34 sstr2 
 |-  ( ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ ( F " ( x i^i A ) ) -> ( ( F " ( x i^i A ) ) C_ y -> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) )
35 33 34 syl 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F " ( x i^i A ) ) C_ y -> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) )
36 29 35 anim12d 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) -> ( P e. ( x i^i ( ( int ` J ) ` A ) ) /\ ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) )
37 26 36 anim12d 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( x e. J /\ ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) -> ( ( x i^i ( ( int ` J ) ` A ) ) e. J /\ ( P e. ( x i^i ( ( int ` J ) ` A ) ) /\ ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) ) )
38 eleq2 
 |-  ( z = ( x i^i ( ( int ` J ) ` A ) ) -> ( P e. z <-> P e. ( x i^i ( ( int ` J ) ` A ) ) ) )
39 imaeq2 
 |-  ( z = ( x i^i ( ( int ` J ) ` A ) ) -> ( F " z ) = ( F " ( x i^i ( ( int ` J ) ` A ) ) ) )
40 39 sseq1d 
 |-  ( z = ( x i^i ( ( int ` J ) ` A ) ) -> ( ( F " z ) C_ y <-> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) )
41 38 40 anbi12d 
 |-  ( z = ( x i^i ( ( int ` J ) ` A ) ) -> ( ( P e. z /\ ( F " z ) C_ y ) <-> ( P e. ( x i^i ( ( int ` J ) ` A ) ) /\ ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) )
42 41 rspcev 
 |-  ( ( ( x i^i ( ( int ` J ) ` A ) ) e. J /\ ( P e. ( x i^i ( ( int ` J ) ` A ) ) /\ ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) )
43 37 42 syl6 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( x e. J /\ ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) )
44 43 expdimp 
 |-  ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ x e. J ) -> ( ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) )
45 44 rexlimdva 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) )
46 eleq2 
 |-  ( z = x -> ( P e. z <-> P e. x ) )
47 imaeq2 
 |-  ( z = x -> ( F " z ) = ( F " x ) )
48 47 sseq1d 
 |-  ( z = x -> ( ( F " z ) C_ y <-> ( F " x ) C_ y ) )
49 46 48 anbi12d 
 |-  ( z = x -> ( ( P e. z /\ ( F " z ) C_ y ) <-> ( P e. x /\ ( F " x ) C_ y ) ) )
50 49 cbvrexvw 
 |-  ( E. z e. J ( P e. z /\ ( F " z ) C_ y ) <-> E. x e. J ( P e. x /\ ( F " x ) C_ y ) )
51 45 50 imbitrdi 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) )
52 19 51 impbid2 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) <-> E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) )
53 vex 
 |-  x e. _V
54 53 inex1 
 |-  ( x i^i A ) e. _V
55 54 a1i 
 |-  ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ x e. J ) -> ( x i^i A ) e. _V )
56 20 uniexd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> U. J e. _V )
57 simp1r 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> A C_ X )
58 57 1 sseqtrdi 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> A C_ U. J )
59 56 58 ssexd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> A e. _V )
60 elrest 
 |-  ( ( J e. Top /\ A e. _V ) -> ( z e. ( J |`t A ) <-> E. x e. J z = ( x i^i A ) ) )
61 20 59 60 syl2anc 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( z e. ( J |`t A ) <-> E. x e. J z = ( x i^i A ) ) )
62 eleq2 
 |-  ( z = ( x i^i A ) -> ( P e. z <-> P e. ( x i^i A ) ) )
63 elin 
 |-  ( P e. ( x i^i A ) <-> ( P e. x /\ P e. A ) )
64 63 rbaib 
 |-  ( P e. A -> ( P e. ( x i^i A ) <-> P e. x ) )
65 10 64 syl 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( P e. ( x i^i A ) <-> P e. x ) )
66 62 65 sylan9bbr 
 |-  ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( P e. z <-> P e. x ) )
67 simpr 
 |-  ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> z = ( x i^i A ) )
68 67 imaeq2d 
 |-  ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( ( F |` A ) " z ) = ( ( F |` A ) " ( x i^i A ) ) )
69 inss2 
 |-  ( x i^i A ) C_ A
70 resima2 
 |-  ( ( x i^i A ) C_ A -> ( ( F |` A ) " ( x i^i A ) ) = ( F " ( x i^i A ) ) )
71 69 70 ax-mp 
 |-  ( ( F |` A ) " ( x i^i A ) ) = ( F " ( x i^i A ) )
72 68 71 eqtrdi 
 |-  ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( ( F |` A ) " z ) = ( F " ( x i^i A ) ) )
73 72 sseq1d 
 |-  ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( ( ( F |` A ) " z ) C_ y <-> ( F " ( x i^i A ) ) C_ y ) )
74 66 73 anbi12d 
 |-  ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( ( P e. z /\ ( ( F |` A ) " z ) C_ y ) <-> ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) )
75 55 61 74 rexxfr2d 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) <-> E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) )
76 52 75 bitr4d 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) <-> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) )
77 13 76 imbi12d 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) <-> ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) )
78 77 ralbidv 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) <-> A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) )
79 simp2r 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> F : X --> Y )
80 simp3 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> K e. Top )
81 57 10 sseldd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> P e. X )
82 1 2 iscnp2 
 |-  ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. X ) /\ ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
83 82 baib 
 |-  ( ( J e. Top /\ K e. Top /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
84 20 80 81 83 syl3anc 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
85 79 84 mpbirand 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F e. ( ( J CnP K ) ` P ) <-> A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) )
86 79 57 fssresd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F |` A ) : A --> Y )
87 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
88 20 87 sylib 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> J e. ( TopOn ` X ) )
89 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
90 88 57 89 syl2anc 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( J |`t A ) e. ( TopOn ` A ) )
91 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
92 80 91 sylib 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> K e. ( TopOn ` Y ) )
93 iscnp 
 |-  ( ( ( J |`t A ) e. ( TopOn ` A ) /\ K e. ( TopOn ` Y ) /\ P e. A ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> ( ( F |` A ) : A --> Y /\ A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) )
94 90 92 10 93 syl3anc 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> ( ( F |` A ) : A --> Y /\ A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) )
95 86 94 mpbirand 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) )
96 78 85 95 3bitr4d 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) ) )
97 96 3expia 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( K e. Top -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) ) ) )
98 4 6 97 pm5.21ndd 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) ) )