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

Metamath Proof Explorer

Theorem txcnmpt

Proof