Metamath Proof Explorer

Theorem 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 fvmptelrn 
 |-  ( ( 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 fvmptelrn 
 |-  ( ( 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 ) ) )