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 syl6ib
 |-  ( ( ( 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 ) ) )