Metamath Proof Explorer

Theorem cnprest2

Description: Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 21-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 cnprest.1 
 |-  X = U. J
2 cnprest.2 
 |-  Y = U. K
3 cnptop1 
 |-  ( F e. ( ( J CnP K ) ` P ) -> J e. Top )
4 1 cnprcl 
 |-  ( F e. ( ( J CnP K ) ` P ) -> P e. X )
5 3 4 jca 
 |-  ( F e. ( ( J CnP K ) ` P ) -> ( J e. Top /\ P e. X ) )
6 5 a1i 
 |-  ( ( K e. Top /\ F : X --> B /\ B C_ Y ) -> ( F e. ( ( J CnP K ) ` P ) -> ( J e. Top /\ P e. X ) ) )
7 cnptop1 
 |-  ( F e. ( ( J CnP ( K |`t B ) ) ` P ) -> J e. Top )
8 1 cnprcl 
 |-  ( F e. ( ( J CnP ( K |`t B ) ) ` P ) -> P e. X )
9 7 8 jca 
 |-  ( F e. ( ( J CnP ( K |`t B ) ) ` P ) -> ( J e. Top /\ P e. X ) )
10 9 a1i 
 |-  ( ( K e. Top /\ F : X --> B /\ B C_ Y ) -> ( F e. ( ( J CnP ( K |`t B ) ) ` P ) -> ( J e. Top /\ P e. X ) ) )
11 simpl2 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> F : X --> B )
12 simprr 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> P e. X )
13 11 12 ffvelcdmd 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( F ` P ) e. B )
14 13 biantrud 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( ( F ` P ) e. x <-> ( ( F ` P ) e. x /\ ( F ` P ) e. B ) ) )
15 elin 
 |-  ( ( F ` P ) e. ( x i^i B ) <-> ( ( F ` P ) e. x /\ ( F ` P ) e. B ) )
16 14 15 bitr4di 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( ( F ` P ) e. x <-> ( F ` P ) e. ( x i^i B ) ) )
17 imassrn 
 |-  ( F " y ) C_ ran F
18 11 frnd 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ran F C_ B )
19 17 18 sstrid 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( F " y ) C_ B )
20 19 biantrud 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( ( F " y ) C_ x <-> ( ( F " y ) C_ x /\ ( F " y ) C_ B ) ) )
21 ssin 
 |-  ( ( ( F " y ) C_ x /\ ( F " y ) C_ B ) <-> ( F " y ) C_ ( x i^i B ) )
22 20 21 bitrdi 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( ( F " y ) C_ x <-> ( F " y ) C_ ( x i^i B ) ) )
23 22 anbi2d 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( ( P e. y /\ ( F " y ) C_ x ) <-> ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) )
24 23 rexbidv 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( E. y e. J ( P e. y /\ ( F " y ) C_ x ) <-> E. y e. J ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) )
25 16 24 imbi12d 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( ( ( F ` P ) e. x -> E. y e. J ( P e. y /\ ( F " y ) C_ x ) ) <-> ( ( F ` P ) e. ( x i^i B ) -> E. y e. J ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) ) )
26 25 ralbidv 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( A. x e. K ( ( F ` P ) e. x -> E. y e. J ( P e. y /\ ( F " y ) C_ x ) ) <-> A. x e. K ( ( F ` P ) e. ( x i^i B ) -> E. y e. J ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) ) )
27 vex 
 |-  x e. _V
28 27 inex1 
 |-  ( x i^i B ) e. _V
29 28 a1i 
 |-  ( ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) /\ x e. K ) -> ( x i^i B ) e. _V )
30 simpl1 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> K e. Top )
31 uniexg 
 |-  ( K e. Top -> U. K e. _V )
32 2 31 eqeltrid 
 |-  ( K e. Top -> Y e. _V )
33 30 32 syl 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> Y e. _V )
34 simpl3 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> B C_ Y )
35 33 34 ssexd 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> B e. _V )
36 elrest 
 |-  ( ( K e. Top /\ B e. _V ) -> ( z e. ( K |`t B ) <-> E. x e. K z = ( x i^i B ) ) )
37 30 35 36 syl2anc 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( z e. ( K |`t B ) <-> E. x e. K z = ( x i^i B ) ) )
38 eleq2 
 |-  ( z = ( x i^i B ) -> ( ( F ` P ) e. z <-> ( F ` P ) e. ( x i^i B ) ) )
39 sseq2 
 |-  ( z = ( x i^i B ) -> ( ( F " y ) C_ z <-> ( F " y ) C_ ( x i^i B ) ) )
40 39 anbi2d 
 |-  ( z = ( x i^i B ) -> ( ( P e. y /\ ( F " y ) C_ z ) <-> ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) )
41 40 rexbidv 
 |-  ( z = ( x i^i B ) -> ( E. y e. J ( P e. y /\ ( F " y ) C_ z ) <-> E. y e. J ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) )
42 38 41 imbi12d 
 |-  ( z = ( x i^i B ) -> ( ( ( F ` P ) e. z -> E. y e. J ( P e. y /\ ( F " y ) C_ z ) ) <-> ( ( F ` P ) e. ( x i^i B ) -> E. y e. J ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) ) )
43 42 adantl 
 |-  ( ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) /\ z = ( x i^i B ) ) -> ( ( ( F ` P ) e. z -> E. y e. J ( P e. y /\ ( F " y ) C_ z ) ) <-> ( ( F ` P ) e. ( x i^i B ) -> E. y e. J ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) ) )
44 29 37 43 ralxfr2d 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( A. z e. ( K |`t B ) ( ( F ` P ) e. z -> E. y e. J ( P e. y /\ ( F " y ) C_ z ) ) <-> A. x e. K ( ( F ` P ) e. ( x i^i B ) -> E. y e. J ( P e. y /\ ( F " y ) C_ ( x i^i B ) ) ) ) )
45 26 44 bitr4d 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( A. x e. K ( ( F ` P ) e. x -> E. y e. J ( P e. y /\ ( F " y ) C_ x ) ) <-> A. z e. ( K |`t B ) ( ( F ` P ) e. z -> E. y e. J ( P e. y /\ ( F " y ) C_ z ) ) ) )
46 11 34 fssd 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> F : X --> Y )
47 simprl 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> J e. Top )
48 1 2 iscnp2 
 |-  ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. X ) /\ ( F : X --> Y /\ A. x e. K ( ( F ` P ) e. x -> E. y e. J ( P e. y /\ ( F " y ) C_ x ) ) ) ) )
49 48 baib 
 |-  ( ( J e. Top /\ K e. Top /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. x e. K ( ( F ` P ) e. x -> E. y e. J ( P e. y /\ ( F " y ) C_ x ) ) ) ) )
50 47 30 12 49 syl3anc 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. x e. K ( ( F ` P ) e. x -> E. y e. J ( P e. y /\ ( F " y ) C_ x ) ) ) ) )
51 46 50 mpbirand 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> A. x e. K ( ( F ` P ) e. x -> E. y e. J ( P e. y /\ ( F " y ) C_ x ) ) ) )
52 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
53 47 52 sylib 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> J e. ( TopOn ` X ) )
54 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
55 30 54 sylib 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> K e. ( TopOn ` Y ) )
56 resttopon 
 |-  ( ( K e. ( TopOn ` Y ) /\ B C_ Y ) -> ( K |`t B ) e. ( TopOn ` B ) )
57 55 34 56 syl2anc 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( K |`t B ) e. ( TopOn ` B ) )
58 iscnp 
 |-  ( ( J e. ( TopOn ` X ) /\ ( K |`t B ) e. ( TopOn ` B ) /\ P e. X ) -> ( F e. ( ( J CnP ( K |`t B ) ) ` P ) <-> ( F : X --> B /\ A. z e. ( K |`t B ) ( ( F ` P ) e. z -> E. y e. J ( P e. y /\ ( F " y ) C_ z ) ) ) ) )
59 53 57 12 58 syl3anc 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( F e. ( ( J CnP ( K |`t B ) ) ` P ) <-> ( F : X --> B /\ A. z e. ( K |`t B ) ( ( F ` P ) e. z -> E. y e. J ( P e. y /\ ( F " y ) C_ z ) ) ) ) )
60 11 59 mpbirand 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( F e. ( ( J CnP ( K |`t B ) ) ` P ) <-> A. z e. ( K |`t B ) ( ( F ` P ) e. z -> E. y e. J ( P e. y /\ ( F " y ) C_ z ) ) ) )
61 45 51 60 3bitr4d 
 |-  ( ( ( K e. Top /\ F : X --> B /\ B C_ Y ) /\ ( J e. Top /\ P e. X ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> F e. ( ( J CnP ( K |`t B ) ) ` P ) ) )
62 61 ex 
 |-  ( ( K e. Top /\ F : X --> B /\ B C_ Y ) -> ( ( J e. Top /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> F e. ( ( J CnP ( K |`t B ) ) ` P ) ) ) )
63 6 10 62 pm5.21ndd 
 |-  ( ( K e. Top /\ F : X --> B /\ B C_ Y ) -> ( F e. ( ( J CnP K ) ` P ) <-> F e. ( ( J CnP ( K |`t B ) ) ` P ) ) )