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