Metamath Proof Explorer

Theorem cnpresti

Description: One direction of cnprest under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Hypothesis cnprest.1 
|- X = U. J
Assertion cnpresti 
|- ( ( A C_ X /\ P e. A /\ 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 eqid 
 |-  U. K = U. K
3 1 2 cnpf 
 |-  ( F e. ( ( J CnP K ) ` P ) -> F : X --> U. K )
4 3 3ad2ant3 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> U. K )
5 simp1 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> A C_ X )
6 4 5 fssresd 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( F |` A ) : A --> U. K )
7 simpl2 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> P e. A )
8 7 fvresd 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( F |` A ) ` P ) = ( F ` P ) )
9 8 eleq1d 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( ( F |` A ) ` P ) e. y <-> ( F ` P ) e. y ) )
10 cnpimaex 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ y e. K /\ ( F ` P ) e. y ) -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) )
11 10 3expia 
 |-  ( ( F e. ( ( J CnP K ) ` P ) /\ y e. K ) -> ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) )
12 11 3ad2antl3 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) )
13 idd 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( P e. x -> P e. x ) )
14 simp2 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> P e. A )
15 13 14 jctird 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( P e. x -> ( P e. x /\ P e. A ) ) )
16 elin 
 |-  ( P e. ( x i^i A ) <-> ( P e. x /\ P e. A ) )
17 15 16 syl6ibr 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( P e. x -> P e. ( x i^i A ) ) )
18 inss1 
 |-  ( x i^i A ) C_ x
19 imass2 
 |-  ( ( x i^i A ) C_ x -> ( F " ( x i^i A ) ) C_ ( F " x ) )
20 18 19 ax-mp 
 |-  ( F " ( x i^i A ) ) C_ ( F " x )
21 id 
 |-  ( ( F " x ) C_ y -> ( F " x ) C_ y )
22 20 21 sstrid 
 |-  ( ( F " x ) C_ y -> ( F " ( x i^i A ) ) C_ y )
23 17 22 anim12d1 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( ( P e. x /\ ( F " x ) C_ y ) -> ( P e. ( x i^i A ) /\ ( F " ( x i^i A ) ) C_ y ) ) )
24 23 reximdv 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. x e. J ( P e. ( x i^i A ) /\ ( F " ( x i^i A ) ) C_ y ) ) )
25 vex 
 |-  x e. _V
26 25 inex1 
 |-  ( x i^i A ) e. _V
27 26 a1i 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ x e. J ) -> ( x i^i A ) e. _V )
28 cnptop1 
 |-  ( F e. ( ( J CnP K ) ` P ) -> J e. Top )
29 28 3ad2ant3 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> J e. Top )
30 29 uniexd 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> U. J e. _V )
31 5 1 sseqtrdi 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> A C_ U. J )
32 30 31 ssexd 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> A e. _V )
33 elrest 
 |-  ( ( J e. Top /\ A e. _V ) -> ( z e. ( J |`t A ) <-> E. x e. J z = ( x i^i A ) ) )
34 29 32 33 syl2anc 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( z e. ( J |`t A ) <-> E. x e. J z = ( x i^i A ) ) )
35 simpr 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> z = ( x i^i A ) )
36 35 eleq2d 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( P e. z <-> P e. ( x i^i A ) ) )
37 35 imaeq2d 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( ( F |` A ) " z ) = ( ( F |` A ) " ( x i^i A ) ) )
38 inss2 
 |-  ( x i^i A ) C_ A
39 resima2 
 |-  ( ( x i^i A ) C_ A -> ( ( F |` A ) " ( x i^i A ) ) = ( F " ( x i^i A ) ) )
40 38 39 ax-mp 
 |-  ( ( F |` A ) " ( x i^i A ) ) = ( F " ( x i^i A ) )
41 37 40 eqtrdi 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( ( F |` A ) " z ) = ( F " ( x i^i A ) ) )
42 41 sseq1d 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( ( ( F |` A ) " z ) C_ y <-> ( F " ( x i^i A ) ) C_ y ) )
43 36 42 anbi12d 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( ( P e. z /\ ( ( F |` A ) " z ) C_ y ) <-> ( P e. ( x i^i A ) /\ ( F " ( x i^i A ) ) C_ y ) ) )
44 27 34 43 rexxfr2d 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) <-> E. x e. J ( P e. ( x i^i A ) /\ ( F " ( x i^i A ) ) C_ y ) ) )
45 24 44 sylibrd 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( 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 ) ) )
46 45 adantr 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( 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 ) ) )
47 12 46 syld 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( F ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) )
48 9 47 sylbid 
 |-  ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) )
49 48 ralrimiva 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J 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 ) ) )
50 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
51 29 50 sylib 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> J e. ( TopOn ` X ) )
52 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
53 51 5 52 syl2anc 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( J |`t A ) e. ( TopOn ` A ) )
54 cnptop2 
 |-  ( F e. ( ( J CnP K ) ` P ) -> K e. Top )
55 54 3ad2ant3 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> K e. Top )
56 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
57 55 56 sylib 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> K e. ( TopOn ` U. K ) )
58 iscnp 
 |-  ( ( ( J |`t A ) e. ( TopOn ` A ) /\ K e. ( TopOn ` U. K ) /\ P e. A ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> ( ( F |` A ) : A --> U. K /\ A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) )
59 53 57 14 58 syl3anc 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> ( ( F |` A ) : A --> U. K /\ A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) )
60 6 49 59 mpbir2and 
 |-  ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) )