Metamath Proof Explorer

Theorem txcnmpt

Description: A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses txcnmpt.1 
|- W = U. U
txcnmpt.2 
|- H = ( x e. W |-> <. ( F ` x ) , ( G ` x ) >. )
Assertion txcnmpt 
|- ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> H e. ( U Cn ( R tX S ) ) )

Proof

Step Hyp Ref Expression
1 txcnmpt.1 
 |-  W = U. U
2 txcnmpt.2 
 |-  H = ( x e. W |-> <. ( F ` x ) , ( G ` x ) >. )
3 eqid 
 |-  U. R = U. R
4 1 3 cnf 
 |-  ( F e. ( U Cn R ) -> F : W --> U. R )
5 4 adantr 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> F : W --> U. R )
6 5 ffvelcdmda 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ x e. W ) -> ( F ` x ) e. U. R )
7 eqid 
 |-  U. S = U. S
8 1 7 cnf 
 |-  ( G e. ( U Cn S ) -> G : W --> U. S )
9 8 adantl 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> G : W --> U. S )
10 9 ffvelcdmda 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ x e. W ) -> ( G ` x ) e. U. S )
11 6 10 opelxpd 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ x e. W ) -> <. ( F ` x ) , ( G ` x ) >. e. ( U. R X. U. S ) )
12 11 2 fmptd 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> H : W --> ( U. R X. U. S ) )
13 2 mptpreima 
 |-  ( `' H " ( r X. s ) ) = { x e. W | <. ( F ` x ) , ( G ` x ) >. e. ( r X. s ) }
14 5 adantr 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> F : W --> U. R )
15 14 adantr 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> F : W --> U. R )
16 ffn 
 |-  ( F : W --> U. R -> F Fn W )
17 elpreima 
 |-  ( F Fn W -> ( x e. ( `' F " r ) <-> ( x e. W /\ ( F ` x ) e. r ) ) )
18 15 16 17 3syl 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> ( x e. ( `' F " r ) <-> ( x e. W /\ ( F ` x ) e. r ) ) )
19 ibar 
 |-  ( x e. W -> ( ( F ` x ) e. r <-> ( x e. W /\ ( F ` x ) e. r ) ) )
20 19 adantl 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> ( ( F ` x ) e. r <-> ( x e. W /\ ( F ` x ) e. r ) ) )
21 18 20 bitr4d 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> ( x e. ( `' F " r ) <-> ( F ` x ) e. r ) )
22 9 ad2antrr 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> G : W --> U. S )
23 ffn 
 |-  ( G : W --> U. S -> G Fn W )
24 elpreima 
 |-  ( G Fn W -> ( x e. ( `' G " s ) <-> ( x e. W /\ ( G ` x ) e. s ) ) )
25 22 23 24 3syl 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> ( x e. ( `' G " s ) <-> ( x e. W /\ ( G ` x ) e. s ) ) )
26 ibar 
 |-  ( x e. W -> ( ( G ` x ) e. s <-> ( x e. W /\ ( G ` x ) e. s ) ) )
27 26 adantl 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> ( ( G ` x ) e. s <-> ( x e. W /\ ( G ` x ) e. s ) ) )
28 25 27 bitr4d 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> ( x e. ( `' G " s ) <-> ( G ` x ) e. s ) )
29 21 28 anbi12d 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> ( ( x e. ( `' F " r ) /\ x e. ( `' G " s ) ) <-> ( ( F ` x ) e. r /\ ( G ` x ) e. s ) ) )
30 elin 
 |-  ( x e. ( ( `' F " r ) i^i ( `' G " s ) ) <-> ( x e. ( `' F " r ) /\ x e. ( `' G " s ) ) )
31 opelxp 
 |-  ( <. ( F ` x ) , ( G ` x ) >. e. ( r X. s ) <-> ( ( F ` x ) e. r /\ ( G ` x ) e. s ) )
32 29 30 31 3bitr4g 
 |-  ( ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) /\ x e. W ) -> ( x e. ( ( `' F " r ) i^i ( `' G " s ) ) <-> <. ( F ` x ) , ( G ` x ) >. e. ( r X. s ) ) )
33 32 rabbi2dva 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> ( W i^i ( ( `' F " r ) i^i ( `' G " s ) ) ) = { x e. W | <. ( F ` x ) , ( G ` x ) >. e. ( r X. s ) } )
34 inss1 
 |-  ( ( `' F " r ) i^i ( `' G " s ) ) C_ ( `' F " r )
35 cnvimass 
 |-  ( `' F " r ) C_ dom F
36 34 35 sstri 
 |-  ( ( `' F " r ) i^i ( `' G " s ) ) C_ dom F
37 36 14 fssdm 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( `' F " r ) i^i ( `' G " s ) ) C_ W )
38 sseqin2 
 |-  ( ( ( `' F " r ) i^i ( `' G " s ) ) C_ W <-> ( W i^i ( ( `' F " r ) i^i ( `' G " s ) ) ) = ( ( `' F " r ) i^i ( `' G " s ) ) )
39 37 38 sylib 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> ( W i^i ( ( `' F " r ) i^i ( `' G " s ) ) ) = ( ( `' F " r ) i^i ( `' G " s ) ) )
40 33 39 eqtr3d 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> { x e. W | <. ( F ` x ) , ( G ` x ) >. e. ( r X. s ) } = ( ( `' F " r ) i^i ( `' G " s ) ) )
41 13 40 eqtrid 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> ( `' H " ( r X. s ) ) = ( ( `' F " r ) i^i ( `' G " s ) ) )
42 cntop1 
 |-  ( G e. ( U Cn S ) -> U e. Top )
43 42 adantl 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> U e. Top )
44 43 adantr 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> U e. Top )
45 cnima 
 |-  ( ( F e. ( U Cn R ) /\ r e. R ) -> ( `' F " r ) e. U )
46 45 ad2ant2r 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> ( `' F " r ) e. U )
47 cnima 
 |-  ( ( G e. ( U Cn S ) /\ s e. S ) -> ( `' G " s ) e. U )
48 47 ad2ant2l 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> ( `' G " s ) e. U )
49 inopn 
 |-  ( ( U e. Top /\ ( `' F " r ) e. U /\ ( `' G " s ) e. U ) -> ( ( `' F " r ) i^i ( `' G " s ) ) e. U )
50 44 46 48 49 syl3anc 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> ( ( `' F " r ) i^i ( `' G " s ) ) e. U )
51 41 50 eqeltrd 
 |-  ( ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) /\ ( r e. R /\ s e. S ) ) -> ( `' H " ( r X. s ) ) e. U )
52 51 ralrimivva 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> A. r e. R A. s e. S ( `' H " ( r X. s ) ) e. U )
53 vex 
 |-  r e. _V
54 vex 
 |-  s e. _V
55 53 54 xpex 
 |-  ( r X. s ) e. _V
56 55 rgen2w 
 |-  A. r e. R A. s e. S ( r X. s ) e. _V
57 eqid 
 |-  ( r e. R , s e. S |-> ( r X. s ) ) = ( r e. R , s e. S |-> ( r X. s ) )
58 imaeq2 
 |-  ( z = ( r X. s ) -> ( `' H " z ) = ( `' H " ( r X. s ) ) )
59 58 eleq1d 
 |-  ( z = ( r X. s ) -> ( ( `' H " z ) e. U <-> ( `' H " ( r X. s ) ) e. U ) )
60 57 59 ralrnmpo 
 |-  ( A. r e. R A. s e. S ( r X. s ) e. _V -> ( A. z e. ran ( r e. R , s e. S |-> ( r X. s ) ) ( `' H " z ) e. U <-> A. r e. R A. s e. S ( `' H " ( r X. s ) ) e. U ) )
61 56 60 ax-mp 
 |-  ( A. z e. ran ( r e. R , s e. S |-> ( r X. s ) ) ( `' H " z ) e. U <-> A. r e. R A. s e. S ( `' H " ( r X. s ) ) e. U )
62 52 61 sylibr 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> A. z e. ran ( r e. R , s e. S |-> ( r X. s ) ) ( `' H " z ) e. U )
63 1 toptopon 
 |-  ( U e. Top <-> U e. ( TopOn ` W ) )
64 43 63 sylib 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> U e. ( TopOn ` W ) )
65 cntop2 
 |-  ( F e. ( U Cn R ) -> R e. Top )
66 cntop2 
 |-  ( G e. ( U Cn S ) -> S e. Top )
67 eqid 
 |-  ran ( r e. R , s e. S |-> ( r X. s ) ) = ran ( r e. R , s e. S |-> ( r X. s ) )
68 67 txval 
 |-  ( ( R e. Top /\ S e. Top ) -> ( R tX S ) = ( topGen ` ran ( r e. R , s e. S |-> ( r X. s ) ) ) )
69 65 66 68 syl2an 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( R tX S ) = ( topGen ` ran ( r e. R , s e. S |-> ( r X. s ) ) ) )
70 toptopon2 
 |-  ( R e. Top <-> R e. ( TopOn ` U. R ) )
71 65 70 sylib 
 |-  ( F e. ( U Cn R ) -> R e. ( TopOn ` U. R ) )
72 toptopon2 
 |-  ( S e. Top <-> S e. ( TopOn ` U. S ) )
73 66 72 sylib 
 |-  ( G e. ( U Cn S ) -> S e. ( TopOn ` U. S ) )
74 txtopon 
 |-  ( ( R e. ( TopOn ` U. R ) /\ S e. ( TopOn ` U. S ) ) -> ( R tX S ) e. ( TopOn ` ( U. R X. U. S ) ) )
75 71 73 74 syl2an 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( R tX S ) e. ( TopOn ` ( U. R X. U. S ) ) )
76 64 69 75 tgcn 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> ( H e. ( U Cn ( R tX S ) ) <-> ( H : W --> ( U. R X. U. S ) /\ A. z e. ran ( r e. R , s e. S |-> ( r X. s ) ) ( `' H " z ) e. U ) ) )
77 12 62 76 mpbir2and 
 |-  ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> H e. ( U Cn ( R tX S ) ) )