Metamath Proof Explorer

Theorem ptrescn

Description: Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015)

Ref Expression
Hypotheses ptrescn.1 
|- X = U. J
ptrescn.2 
|- J = ( Xt_ ` F )
ptrescn.3 
|- K = ( Xt_ ` ( F |` B ) )
Assertion ptrescn 
|- ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( x e. X |-> ( x |` B ) ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 ptrescn.1 
 |-  X = U. J
2 ptrescn.2 
 |-  J = ( Xt_ ` F )
3 ptrescn.3 
 |-  K = ( Xt_ ` ( F |` B ) )
4 simpl3 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ x e. X ) -> B C_ A )
5 2 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. J )
6 5 3adant3 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> X_ k e. A U. ( F ` k ) = U. J )
7 6 1 eqtr4di 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> X_ k e. A U. ( F ` k ) = X )
8 7 eleq2d 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( x e. X_ k e. A U. ( F ` k ) <-> x e. X ) )
9 8 biimpar 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ x e. X ) -> x e. X_ k e. A U. ( F ` k ) )
10 resixp 
 |-  ( ( B C_ A /\ x e. X_ k e. A U. ( F ` k ) ) -> ( x |` B ) e. X_ k e. B U. ( F ` k ) )
11 4 9 10 syl2anc 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ x e. X ) -> ( x |` B ) e. X_ k e. B U. ( F ` k ) )
12 ixpeq2 
 |-  ( A. k e. B U. ( ( F |` B ) ` k ) = U. ( F ` k ) -> X_ k e. B U. ( ( F |` B ) ` k ) = X_ k e. B U. ( F ` k ) )
13 fvres 
 |-  ( k e. B -> ( ( F |` B ) ` k ) = ( F ` k ) )
14 13 unieqd 
 |-  ( k e. B -> U. ( ( F |` B ) ` k ) = U. ( F ` k ) )
15 12 14 mprg 
 |-  X_ k e. B U. ( ( F |` B ) ` k ) = X_ k e. B U. ( F ` k )
16 ssexg 
 |-  ( ( B C_ A /\ A e. V ) -> B e. _V )
17 16 ancoms 
 |-  ( ( A e. V /\ B C_ A ) -> B e. _V )
18 17 3adant2 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> B e. _V )
19 fssres 
 |-  ( ( F : A --> Top /\ B C_ A ) -> ( F |` B ) : B --> Top )
20 19 3adant1 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( F |` B ) : B --> Top )
21 3 ptuni 
 |-  ( ( B e. _V /\ ( F |` B ) : B --> Top ) -> X_ k e. B U. ( ( F |` B ) ` k ) = U. K )
22 18 20 21 syl2anc 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> X_ k e. B U. ( ( F |` B ) ` k ) = U. K )
23 15 22 eqtr3id 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> X_ k e. B U. ( F ` k ) = U. K )
24 23 adantr 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ x e. X ) -> X_ k e. B U. ( F ` k ) = U. K )
25 11 24 eleqtrd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ x e. X ) -> ( x |` B ) e. U. K )
26 25 fmpttd 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( x e. X |-> ( x |` B ) ) : X --> U. K )
27 fimacnv 
 |-  ( ( x e. X |-> ( x |` B ) ) : X --> U. K -> ( `' ( x e. X |-> ( x |` B ) ) " U. K ) = X )
28 26 27 syl 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( `' ( x e. X |-> ( x |` B ) ) " U. K ) = X )
29 pttop 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
30 2 29 eqeltrid 
 |-  ( ( A e. V /\ F : A --> Top ) -> J e. Top )
31 30 3adant3 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> J e. Top )
32 1 topopn 
 |-  ( J e. Top -> X e. J )
33 31 32 syl 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> X e. J )
34 28 33 eqeltrd 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( `' ( x e. X |-> ( x |` B ) ) " U. K ) e. J )
35 elsni 
 |-  ( v e. { U. K } -> v = U. K )
36 35 imaeq2d 
 |-  ( v e. { U. K } -> ( `' ( x e. X |-> ( x |` B ) ) " v ) = ( `' ( x e. X |-> ( x |` B ) ) " U. K ) )
37 36 eleq1d 
 |-  ( v e. { U. K } -> ( ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J <-> ( `' ( x e. X |-> ( x |` B ) ) " U. K ) e. J ) )
38 34 37 syl5ibrcom 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( v e. { U. K } -> ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J ) )
39 38 ralrimiv 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> A. v e. { U. K } ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J )
40 imaco 
 |-  ( ( `' ( x e. X |-> ( x |` B ) ) o. `' ( z e. U. K |-> ( z ` k ) ) ) " u ) = ( `' ( x e. X |-> ( x |` B ) ) " ( `' ( z e. U. K |-> ( z ` k ) ) " u ) )
41 cnvco 
 |-  `' ( ( z e. U. K |-> ( z ` k ) ) o. ( x e. X |-> ( x |` B ) ) ) = ( `' ( x e. X |-> ( x |` B ) ) o. `' ( z e. U. K |-> ( z ` k ) ) )
42 25 adantlr 
 |-  ( ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) /\ x e. X ) -> ( x |` B ) e. U. K )
43 eqidd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( x e. X |-> ( x |` B ) ) = ( x e. X |-> ( x |` B ) ) )
44 eqidd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( z e. U. K |-> ( z ` k ) ) = ( z e. U. K |-> ( z ` k ) ) )
45 fveq1 
 |-  ( z = ( x |` B ) -> ( z ` k ) = ( ( x |` B ) ` k ) )
46 42 43 44 45 fmptco 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( ( z e. U. K |-> ( z ` k ) ) o. ( x e. X |-> ( x |` B ) ) ) = ( x e. X |-> ( ( x |` B ) ` k ) ) )
47 fvres 
 |-  ( k e. B -> ( ( x |` B ) ` k ) = ( x ` k ) )
48 47 ad2antrl 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( ( x |` B ) ` k ) = ( x ` k ) )
49 48 mpteq2dv 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( x e. X |-> ( ( x |` B ) ` k ) ) = ( x e. X |-> ( x ` k ) ) )
50 46 49 eqtrd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( ( z e. U. K |-> ( z ` k ) ) o. ( x e. X |-> ( x |` B ) ) ) = ( x e. X |-> ( x ` k ) ) )
51 50 cnveqd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> `' ( ( z e. U. K |-> ( z ` k ) ) o. ( x e. X |-> ( x |` B ) ) ) = `' ( x e. X |-> ( x ` k ) ) )
52 41 51 eqtr3id 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( `' ( x e. X |-> ( x |` B ) ) o. `' ( z e. U. K |-> ( z ` k ) ) ) = `' ( x e. X |-> ( x ` k ) ) )
53 52 imaeq1d 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( ( `' ( x e. X |-> ( x |` B ) ) o. `' ( z e. U. K |-> ( z ` k ) ) ) " u ) = ( `' ( x e. X |-> ( x ` k ) ) " u ) )
54 40 53 eqtr3id 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( `' ( x e. X |-> ( x |` B ) ) " ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) = ( `' ( x e. X |-> ( x ` k ) ) " u ) )
55 simpl1 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> A e. V )
56 simpl2 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> F : A --> Top )
57 simpl3 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> B C_ A )
58 simprl 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> k e. B )
59 57 58 sseldd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> k e. A )
60 1 2 ptpjcn 
 |-  ( ( A e. V /\ F : A --> Top /\ k e. A ) -> ( x e. X |-> ( x ` k ) ) e. ( J Cn ( F ` k ) ) )
61 55 56 59 60 syl3anc 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( x e. X |-> ( x ` k ) ) e. ( J Cn ( F ` k ) ) )
62 simprr 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> u e. ( F ` k ) )
63 cnima 
 |-  ( ( ( x e. X |-> ( x ` k ) ) e. ( J Cn ( F ` k ) ) /\ u e. ( F ` k ) ) -> ( `' ( x e. X |-> ( x ` k ) ) " u ) e. J )
64 61 62 63 syl2anc 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( `' ( x e. X |-> ( x ` k ) ) " u ) e. J )
65 54 64 eqeltrd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( `' ( x e. X |-> ( x |` B ) ) " ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) e. J )
66 imaeq2 
 |-  ( v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) -> ( `' ( x e. X |-> ( x |` B ) ) " v ) = ( `' ( x e. X |-> ( x |` B ) ) " ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) )
67 66 eleq1d 
 |-  ( v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) -> ( ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J <-> ( `' ( x e. X |-> ( x |` B ) ) " ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) e. J ) )
68 65 67 syl5ibrcom 
 |-  ( ( ( A e. V /\ F : A --> Top /\ B C_ A ) /\ ( k e. B /\ u e. ( F ` k ) ) ) -> ( v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) -> ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J ) )
69 68 rexlimdvva 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( E. k e. B E. u e. ( F ` k ) v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) -> ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J ) )
70 69 alrimiv 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> A. v ( E. k e. B E. u e. ( F ` k ) v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) -> ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J ) )
71 eqid 
 |-  ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) = ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) )
72 71 rnmpo 
 |-  ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) = { y | E. k e. B E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) }
73 72 raleqi 
 |-  ( A. v e. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J <-> A. v e. { y | E. k e. B E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) } ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J )
74 13 rexeqdv 
 |-  ( k e. B -> ( E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) <-> E. u e. ( F ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) )
75 eqeq1 
 |-  ( y = v -> ( y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) <-> v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) )
76 75 rexbidv 
 |-  ( y = v -> ( E. u e. ( F ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) <-> E. u e. ( F ` k ) v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) )
77 74 76 sylan9bbr 
 |-  ( ( y = v /\ k e. B ) -> ( E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) <-> E. u e. ( F ` k ) v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) )
78 77 rexbidva 
 |-  ( y = v -> ( E. k e. B E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) <-> E. k e. B E. u e. ( F ` k ) v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) )
79 78 ralab 
 |-  ( A. v e. { y | E. k e. B E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) } ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J <-> A. v ( E. k e. B E. u e. ( F ` k ) v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) -> ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J ) )
80 73 79 bitri 
 |-  ( A. v e. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J <-> A. v ( E. k e. B E. u e. ( F ` k ) v = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) -> ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J ) )
81 70 80 sylibr 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> A. v e. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J )
82 ralunb 
 |-  ( A. v e. ( { U. K } u. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ) ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J <-> ( A. v e. { U. K } ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J /\ A. v e. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J ) )
83 39 81 82 sylanbrc 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> A. v e. ( { U. K } u. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ) ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J )
84 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
85 31 84 sylib 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> J e. ( TopOn ` X ) )
86 snex 
 |-  { U. K } e. _V
87 fvex 
 |-  ( ( F |` B ) ` k ) e. _V
88 87 abrexex 
 |-  { y | E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) } e. _V
89 88 rgenw 
 |-  A. k e. B { y | E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) } e. _V
90 abrexex2g 
 |-  ( ( B e. _V /\ A. k e. B { y | E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) } e. _V ) -> { y | E. k e. B E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) } e. _V )
91 18 89 90 sylancl 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> { y | E. k e. B E. u e. ( ( F |` B ) ` k ) y = ( `' ( z e. U. K |-> ( z ` k ) ) " u ) } e. _V )
92 72 91 eqeltrid 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) e. _V )
93 unexg 
 |-  ( ( { U. K } e. _V /\ ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) e. _V ) -> ( { U. K } u. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ) e. _V )
94 86 92 93 sylancr 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( { U. K } u. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ) e. _V )
95 eqid 
 |-  U. K = U. K
96 3 95 71 ptval2 
 |-  ( ( B e. _V /\ ( F |` B ) : B --> Top ) -> K = ( topGen ` ( fi ` ( { U. K } u. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ) ) ) )
97 18 20 96 syl2anc 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> K = ( topGen ` ( fi ` ( { U. K } u. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ) ) ) )
98 pttop 
 |-  ( ( B e. _V /\ ( F |` B ) : B --> Top ) -> ( Xt_ ` ( F |` B ) ) e. Top )
99 18 20 98 syl2anc 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( Xt_ ` ( F |` B ) ) e. Top )
100 3 99 eqeltrid 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> K e. Top )
101 95 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
102 100 101 sylib 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> K e. ( TopOn ` U. K ) )
103 85 94 97 102 subbascn 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( ( x e. X |-> ( x |` B ) ) e. ( J Cn K ) <-> ( ( x e. X |-> ( x |` B ) ) : X --> U. K /\ A. v e. ( { U. K } u. ran ( k e. B , u e. ( ( F |` B ) ` k ) |-> ( `' ( z e. U. K |-> ( z ` k ) ) " u ) ) ) ( `' ( x e. X |-> ( x |` B ) ) " v ) e. J ) ) )
104 26 83 103 mpbir2and 
 |-  ( ( A e. V /\ F : A --> Top /\ B C_ A ) -> ( x e. X |-> ( x |` B ) ) e. ( J Cn K ) )