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