Metamath Proof Explorer

Theorem cnrest2

Description: Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnrest2 
|- ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t B ) ) ) )

Proof

Step Hyp Ref Expression
1 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
2 1 a1i 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) -> J e. Top ) )
3 eqid 
 |-  U. J = U. J
4 eqid 
 |-  U. K = U. K
5 3 4 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
6 5 ffnd 
 |-  ( F e. ( J Cn K ) -> F Fn U. J )
7 6 a1i 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) -> F Fn U. J ) )
8 simp2 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ran F C_ B )
9 7 8 jctird 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) -> ( F Fn U. J /\ ran F C_ B ) ) )
10 df-f 
 |-  ( F : U. J --> B <-> ( F Fn U. J /\ ran F C_ B ) )
11 9 10 syl6ibr 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) -> F : U. J --> B ) )
12 2 11 jcad 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) -> ( J e. Top /\ F : U. J --> B ) ) )
13 cntop1 
 |-  ( F e. ( J Cn ( K |`t B ) ) -> J e. Top )
14 13 adantl 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ F e. ( J Cn ( K |`t B ) ) ) -> J e. Top )
15 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
16 14 15 sylib 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ F e. ( J Cn ( K |`t B ) ) ) -> J e. ( TopOn ` U. J ) )
17 resttopon 
 |-  ( ( K e. ( TopOn ` Y ) /\ B C_ Y ) -> ( K |`t B ) e. ( TopOn ` B ) )
18 17 3adant2 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( K |`t B ) e. ( TopOn ` B ) )
19 18 adantr 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ F e. ( J Cn ( K |`t B ) ) ) -> ( K |`t B ) e. ( TopOn ` B ) )
20 simpr 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ F e. ( J Cn ( K |`t B ) ) ) -> F e. ( J Cn ( K |`t B ) ) )
21 cnf2 
 |-  ( ( J e. ( TopOn ` U. J ) /\ ( K |`t B ) e. ( TopOn ` B ) /\ F e. ( J Cn ( K |`t B ) ) ) -> F : U. J --> B )
22 16 19 20 21 syl3anc 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ F e. ( J Cn ( K |`t B ) ) ) -> F : U. J --> B )
23 14 22 jca 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ F e. ( J Cn ( K |`t B ) ) ) -> ( J e. Top /\ F : U. J --> B ) )
24 23 ex 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn ( K |`t B ) ) -> ( J e. Top /\ F : U. J --> B ) ) )
25 vex 
 |-  x e. _V
26 25 inex1 
 |-  ( x i^i B ) e. _V
27 26 a1i 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> ( x i^i B ) e. _V )
28 simpl1 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> K e. ( TopOn ` Y ) )
29 toponmax 
 |-  ( K e. ( TopOn ` Y ) -> Y e. K )
30 28 29 syl 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> Y e. K )
31 simpl3 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> B C_ Y )
32 30 31 ssexd 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> B e. _V )
33 elrest 
 |-  ( ( K e. ( TopOn ` Y ) /\ B e. _V ) -> ( y e. ( K |`t B ) <-> E. x e. K y = ( x i^i B ) ) )
34 28 32 33 syl2anc 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( y e. ( K |`t B ) <-> E. x e. K y = ( x i^i B ) ) )
35 imaeq2 
 |-  ( y = ( x i^i B ) -> ( `' F " y ) = ( `' F " ( x i^i B ) ) )
36 35 eleq1d 
 |-  ( y = ( x i^i B ) -> ( ( `' F " y ) e. J <-> ( `' F " ( x i^i B ) ) e. J ) )
37 36 adantl 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ y = ( x i^i B ) ) -> ( ( `' F " y ) e. J <-> ( `' F " ( x i^i B ) ) e. J ) )
38 27 34 37 ralxfr2d 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( A. y e. ( K |`t B ) ( `' F " y ) e. J <-> A. x e. K ( `' F " ( x i^i B ) ) e. J ) )
39 simplrr 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> F : U. J --> B )
40 ffun 
 |-  ( F : U. J --> B -> Fun F )
41 inpreima 
 |-  ( Fun F -> ( `' F " ( x i^i B ) ) = ( ( `' F " x ) i^i ( `' F " B ) ) )
42 39 40 41 3syl 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> ( `' F " ( x i^i B ) ) = ( ( `' F " x ) i^i ( `' F " B ) ) )
43 cnvimass 
 |-  ( `' F " x ) C_ dom F
44 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
45 43 44 sseqtrri 
 |-  ( `' F " x ) C_ ( `' F " ran F )
46 simpll2 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> ran F C_ B )
47 imass2 
 |-  ( ran F C_ B -> ( `' F " ran F ) C_ ( `' F " B ) )
48 46 47 syl 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> ( `' F " ran F ) C_ ( `' F " B ) )
49 45 48 sstrid 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> ( `' F " x ) C_ ( `' F " B ) )
50 df-ss 
 |-  ( ( `' F " x ) C_ ( `' F " B ) <-> ( ( `' F " x ) i^i ( `' F " B ) ) = ( `' F " x ) )
51 49 50 sylib 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> ( ( `' F " x ) i^i ( `' F " B ) ) = ( `' F " x ) )
52 42 51 eqtrd 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> ( `' F " ( x i^i B ) ) = ( `' F " x ) )
53 52 eleq1d 
 |-  ( ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) /\ x e. K ) -> ( ( `' F " ( x i^i B ) ) e. J <-> ( `' F " x ) e. J ) )
54 53 ralbidva 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( A. x e. K ( `' F " ( x i^i B ) ) e. J <-> A. x e. K ( `' F " x ) e. J ) )
55 simprr 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> F : U. J --> B )
56 55 31 fssd 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> F : U. J --> Y )
57 56 biantrurd 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( A. x e. K ( `' F " x ) e. J <-> ( F : U. J --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
58 38 54 57 3bitrrd 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( ( F : U. J --> Y /\ A. x e. K ( `' F " x ) e. J ) <-> A. y e. ( K |`t B ) ( `' F " y ) e. J ) )
59 55 biantrurd 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( A. y e. ( K |`t B ) ( `' F " y ) e. J <-> ( F : U. J --> B /\ A. y e. ( K |`t B ) ( `' F " y ) e. J ) ) )
60 58 59 bitrd 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( ( F : U. J --> Y /\ A. x e. K ( `' F " x ) e. J ) <-> ( F : U. J --> B /\ A. y e. ( K |`t B ) ( `' F " y ) e. J ) ) )
61 simprl 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> J e. Top )
62 61 15 sylib 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> J e. ( TopOn ` U. J ) )
63 iscn 
 |-  ( ( J e. ( TopOn ` U. J ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : U. J --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
64 62 28 63 syl2anc 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( F e. ( J Cn K ) <-> ( F : U. J --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
65 18 adantr 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( K |`t B ) e. ( TopOn ` B ) )
66 iscn 
 |-  ( ( J e. ( TopOn ` U. J ) /\ ( K |`t B ) e. ( TopOn ` B ) ) -> ( F e. ( J Cn ( K |`t B ) ) <-> ( F : U. J --> B /\ A. y e. ( K |`t B ) ( `' F " y ) e. J ) ) )
67 62 65 66 syl2anc 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( F e. ( J Cn ( K |`t B ) ) <-> ( F : U. J --> B /\ A. y e. ( K |`t B ) ( `' F " y ) e. J ) ) )
68 60 64 67 3bitr4d 
 |-  ( ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) /\ ( J e. Top /\ F : U. J --> B ) ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t B ) ) ) )
69 68 ex 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( ( J e. Top /\ F : U. J --> B ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t B ) ) ) ) )
70 12 24 69 pm5.21ndd 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t B ) ) ) )