cnmpt1t

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmptid.j	\|- ( ph -> J e. ( TopOn ` X ) )
	cnmpt11.a	\|- ( ph -> ( x e. X \|-> A ) e. ( J Cn K ) )
	cnmpt1t.b	\|- ( ph -> ( x e. X \|-> B ) e. ( J Cn L ) )
Assertion	cnmpt1t	\|- ( ph -> ( x e. X \|-> <. A , B >. ) e. ( J Cn ( K tX L ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	\|- ( ph -> J e. ( TopOn ` X ) )
2		cnmpt11.a	\|- ( ph -> ( x e. X \|-> A ) e. ( J Cn K ) )
3		cnmpt1t.b	\|- ( ph -> ( x e. X \|-> B ) e. ( J Cn L ) )
4		toponuni	\|- ( J e. ( TopOn ` X ) -> X = U. J )
5		mpteq1	\|- ( X = U. J -> ( x e. X \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) = ( x e. U. J \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) )
6	1 4 5	3syl	\|- ( ph -> ( x e. X \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) = ( x e. U. J \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) )
7		simpr	\|- ( ( ph /\ x e. X ) -> x e. X )
8		cntop2	\|- ( ( x e. X \|-> A ) e. ( J Cn K ) -> K e. Top )
9	2 8	syl	\|- ( ph -> K e. Top )
10		toptopon2	\|- ( K e. Top <-> K e. ( TopOn ` U. K ) )
11	9 10	sylib	\|- ( ph -> K e. ( TopOn ` U. K ) )
12		cnf2	\|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) /\ ( x e. X \|-> A ) e. ( J Cn K ) ) -> ( x e. X \|-> A ) : X --> U. K )
13	1 11 2 12	syl3anc	\|- ( ph -> ( x e. X \|-> A ) : X --> U. K )
14	13	fvmptelcdm	\|- ( ( ph /\ x e. X ) -> A e. U. K )
15		eqid	\|- ( x e. X \|-> A ) = ( x e. X \|-> A )
16	15	fvmpt2	\|- ( ( x e. X /\ A e. U. K ) -> ( ( x e. X \|-> A ) ` x ) = A )
17	7 14 16	syl2anc	\|- ( ( ph /\ x e. X ) -> ( ( x e. X \|-> A ) ` x ) = A )
18		cntop2	\|- ( ( x e. X \|-> B ) e. ( J Cn L ) -> L e. Top )
19	3 18	syl	\|- ( ph -> L e. Top )
20		toptopon2	\|- ( L e. Top <-> L e. ( TopOn ` U. L ) )
21	19 20	sylib	\|- ( ph -> L e. ( TopOn ` U. L ) )
22		cnf2	\|- ( ( J e. ( TopOn ` X ) /\ L e. ( TopOn ` U. L ) /\ ( x e. X \|-> B ) e. ( J Cn L ) ) -> ( x e. X \|-> B ) : X --> U. L )
23	1 21 3 22	syl3anc	\|- ( ph -> ( x e. X \|-> B ) : X --> U. L )
24	23	fvmptelcdm	\|- ( ( ph /\ x e. X ) -> B e. U. L )
25		eqid	\|- ( x e. X \|-> B ) = ( x e. X \|-> B )
26	25	fvmpt2	\|- ( ( x e. X /\ B e. U. L ) -> ( ( x e. X \|-> B ) ` x ) = B )
27	7 24 26	syl2anc	\|- ( ( ph /\ x e. X ) -> ( ( x e. X \|-> B ) ` x ) = B )
28	17 27	opeq12d	\|- ( ( ph /\ x e. X ) -> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. = <. A , B >. )
29	28	mpteq2dva	\|- ( ph -> ( x e. X \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) = ( x e. X \|-> <. A , B >. ) )
30	6 29	eqtr3d	\|- ( ph -> ( x e. U. J \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) = ( x e. X \|-> <. A , B >. ) )
31		eqid	\|- U. J = U. J
32		nfcv	\|- F/_ y <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >.
33		nffvmpt1	\|- F/_ x ( ( x e. X \|-> A ) ` y )
34		nffvmpt1	\|- F/_ x ( ( x e. X \|-> B ) ` y )
35	33 34	nfop	\|- F/_ x <. ( ( x e. X \|-> A ) ` y ) , ( ( x e. X \|-> B ) ` y ) >.
36		fveq2	\|- ( x = y -> ( ( x e. X \|-> A ) ` x ) = ( ( x e. X \|-> A ) ` y ) )
37		fveq2	\|- ( x = y -> ( ( x e. X \|-> B ) ` x ) = ( ( x e. X \|-> B ) ` y ) )
38	36 37	opeq12d	\|- ( x = y -> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. = <. ( ( x e. X \|-> A ) ` y ) , ( ( x e. X \|-> B ) ` y ) >. )
39	32 35 38	cbvmpt	\|- ( x e. U. J \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) = ( y e. U. J \|-> <. ( ( x e. X \|-> A ) ` y ) , ( ( x e. X \|-> B ) ` y ) >. )
40	31 39	txcnmpt	\|- ( ( ( x e. X \|-> A ) e. ( J Cn K ) /\ ( x e. X \|-> B ) e. ( J Cn L ) ) -> ( x e. U. J \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) e. ( J Cn ( K tX L ) ) )
41	2 3 40	syl2anc	\|- ( ph -> ( x e. U. J \|-> <. ( ( x e. X \|-> A ) ` x ) , ( ( x e. X \|-> B ) ` x ) >. ) e. ( J Cn ( K tX L ) ) )
42	30 41	eqeltrrd	\|- ( ph -> ( x e. X \|-> <. A , B >. ) e. ( J Cn ( K tX L ) ) )

Metamath Proof Explorer

Theorem cnmpt1t

Proof