Metamath Proof Explorer

Theorem cnmpt2t

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 cnmpt21.j 
|- ( ph -> J e. ( TopOn ` X ) )
cnmpt21.k 
|- ( ph -> K e. ( TopOn ` Y ) )
cnmpt21.a 
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
cnmpt2t.b 
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )
Assertion cnmpt2t 
|- ( ph -> ( x e. X , y e. Y |-> <. A , B >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )

Proof

Step Hyp Ref Expression
1 cnmpt21.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmpt21.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 cnmpt21.a 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
4 cnmpt2t.b 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )
5 fveq2 
 |-  ( z = <. u , v >. -> ( ( x e. X , y e. Y |-> A ) ` z ) = ( ( x e. X , y e. Y |-> A ) ` <. u , v >. ) )
6 df-ov 
 |-  ( u ( x e. X , y e. Y |-> A ) v ) = ( ( x e. X , y e. Y |-> A ) ` <. u , v >. )
7 5 6 eqtr4di 
 |-  ( z = <. u , v >. -> ( ( x e. X , y e. Y |-> A ) ` z ) = ( u ( x e. X , y e. Y |-> A ) v ) )
8 fveq2 
 |-  ( z = <. u , v >. -> ( ( x e. X , y e. Y |-> B ) ` z ) = ( ( x e. X , y e. Y |-> B ) ` <. u , v >. ) )
9 df-ov 
 |-  ( u ( x e. X , y e. Y |-> B ) v ) = ( ( x e. X , y e. Y |-> B ) ` <. u , v >. )
10 8 9 eqtr4di 
 |-  ( z = <. u , v >. -> ( ( x e. X , y e. Y |-> B ) ` z ) = ( u ( x e. X , y e. Y |-> B ) v ) )
11 7 10 opeq12d 
 |-  ( z = <. u , v >. -> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. = <. ( u ( x e. X , y e. Y |-> A ) v ) , ( u ( x e. X , y e. Y |-> B ) v ) >. )
12 11 mpompt 
 |-  ( z e. ( X X. Y ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) = ( u e. X , v e. Y |-> <. ( u ( x e. X , y e. Y |-> A ) v ) , ( u ( x e. X , y e. Y |-> B ) v ) >. )
13 nfcv 
 |-  F/_ x u
14 nfmpo1 
 |-  F/_ x ( x e. X , y e. Y |-> A )
15 nfcv 
 |-  F/_ x v
16 13 14 15 nfov 
 |-  F/_ x ( u ( x e. X , y e. Y |-> A ) v )
17 nfmpo1 
 |-  F/_ x ( x e. X , y e. Y |-> B )
18 13 17 15 nfov 
 |-  F/_ x ( u ( x e. X , y e. Y |-> B ) v )
19 16 18 nfop 
 |-  F/_ x <. ( u ( x e. X , y e. Y |-> A ) v ) , ( u ( x e. X , y e. Y |-> B ) v ) >.
20 nfcv 
 |-  F/_ y u
21 nfmpo2 
 |-  F/_ y ( x e. X , y e. Y |-> A )
22 nfcv 
 |-  F/_ y v
23 20 21 22 nfov 
 |-  F/_ y ( u ( x e. X , y e. Y |-> A ) v )
24 nfmpo2 
 |-  F/_ y ( x e. X , y e. Y |-> B )
25 20 24 22 nfov 
 |-  F/_ y ( u ( x e. X , y e. Y |-> B ) v )
26 23 25 nfop 
 |-  F/_ y <. ( u ( x e. X , y e. Y |-> A ) v ) , ( u ( x e. X , y e. Y |-> B ) v ) >.
27 nfcv 
 |-  F/_ u <. ( x ( x e. X , y e. Y |-> A ) y ) , ( x ( x e. X , y e. Y |-> B ) y ) >.
28 nfcv 
 |-  F/_ v <. ( x ( x e. X , y e. Y |-> A ) y ) , ( x ( x e. X , y e. Y |-> B ) y ) >.
29 oveq12 
 |-  ( ( u = x /\ v = y ) -> ( u ( x e. X , y e. Y |-> A ) v ) = ( x ( x e. X , y e. Y |-> A ) y ) )
30 oveq12 
 |-  ( ( u = x /\ v = y ) -> ( u ( x e. X , y e. Y |-> B ) v ) = ( x ( x e. X , y e. Y |-> B ) y ) )
31 29 30 opeq12d 
 |-  ( ( u = x /\ v = y ) -> <. ( u ( x e. X , y e. Y |-> A ) v ) , ( u ( x e. X , y e. Y |-> B ) v ) >. = <. ( x ( x e. X , y e. Y |-> A ) y ) , ( x ( x e. X , y e. Y |-> B ) y ) >. )
32 19 26 27 28 31 cbvmpo 
 |-  ( u e. X , v e. Y |-> <. ( u ( x e. X , y e. Y |-> A ) v ) , ( u ( x e. X , y e. Y |-> B ) v ) >. ) = ( x e. X , y e. Y |-> <. ( x ( x e. X , y e. Y |-> A ) y ) , ( x ( x e. X , y e. Y |-> B ) y ) >. )
33 12 32 eqtri 
 |-  ( z e. ( X X. Y ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) = ( x e. X , y e. Y |-> <. ( x ( x e. X , y e. Y |-> A ) y ) , ( x ( x e. X , y e. Y |-> B ) y ) >. )
34 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
35 1 2 34 syl2anc 
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
36 toponuni 
 |-  ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) -> ( X X. Y ) = U. ( J tX K ) )
37 mpteq1 
 |-  ( ( X X. Y ) = U. ( J tX K ) -> ( z e. ( X X. Y ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) = ( z e. U. ( J tX K ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) )
38 35 36 37 3syl 
 |-  ( ph -> ( z e. ( X X. Y ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) = ( z e. U. ( J tX K ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) )
39 simp2 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> x e. X )
40 simp3 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> y e. Y )
41 cntop2 
 |-  ( ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) -> L e. Top )
42 3 41 syl 
 |-  ( ph -> L e. Top )
43 toptopon2 
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
44 42 43 sylib 
 |-  ( ph -> L e. ( TopOn ` U. L ) )
45 cnf2 
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` U. L ) /\ ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> U. L )
46 35 44 3 45 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> U. L )
47 eqid 
 |-  ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A )
48 47 fmpo 
 |-  ( A. x e. X A. y e. Y A e. U. L <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> U. L )
49 46 48 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y A e. U. L )
50 rsp2 
 |-  ( A. x e. X A. y e. Y A e. U. L -> ( ( x e. X /\ y e. Y ) -> A e. U. L ) )
51 49 50 syl 
 |-  ( ph -> ( ( x e. X /\ y e. Y ) -> A e. U. L ) )
52 51 3impib 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> A e. U. L )
53 47 ovmpt4g 
 |-  ( ( x e. X /\ y e. Y /\ A e. U. L ) -> ( x ( x e. X , y e. Y |-> A ) y ) = A )
54 39 40 52 53 syl3anc 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( x ( x e. X , y e. Y |-> A ) y ) = A )
55 cntop2 
 |-  ( ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) -> M e. Top )
56 4 55 syl 
 |-  ( ph -> M e. Top )
57 toptopon2 
 |-  ( M e. Top <-> M e. ( TopOn ` U. M ) )
58 56 57 sylib 
 |-  ( ph -> M e. ( TopOn ` U. M ) )
59 cnf2 
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ M e. ( TopOn ` U. M ) /\ ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) ) -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> U. M )
60 35 58 4 59 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> U. M )
61 eqid 
 |-  ( x e. X , y e. Y |-> B ) = ( x e. X , y e. Y |-> B )
62 61 fmpo 
 |-  ( A. x e. X A. y e. Y B e. U. M <-> ( x e. X , y e. Y |-> B ) : ( X X. Y ) --> U. M )
63 60 62 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y B e. U. M )
64 rsp2 
 |-  ( A. x e. X A. y e. Y B e. U. M -> ( ( x e. X /\ y e. Y ) -> B e. U. M ) )
65 63 64 syl 
 |-  ( ph -> ( ( x e. X /\ y e. Y ) -> B e. U. M ) )
66 65 3impib 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> B e. U. M )
67 61 ovmpt4g 
 |-  ( ( x e. X /\ y e. Y /\ B e. U. M ) -> ( x ( x e. X , y e. Y |-> B ) y ) = B )
68 39 40 66 67 syl3anc 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( x ( x e. X , y e. Y |-> B ) y ) = B )
69 54 68 opeq12d 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> <. ( x ( x e. X , y e. Y |-> A ) y ) , ( x ( x e. X , y e. Y |-> B ) y ) >. = <. A , B >. )
70 69 mpoeq3dva 
 |-  ( ph -> ( x e. X , y e. Y |-> <. ( x ( x e. X , y e. Y |-> A ) y ) , ( x ( x e. X , y e. Y |-> B ) y ) >. ) = ( x e. X , y e. Y |-> <. A , B >. ) )
71 33 38 70 3eqtr3a 
 |-  ( ph -> ( z e. U. ( J tX K ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) = ( x e. X , y e. Y |-> <. A , B >. ) )
72 eqid 
 |-  U. ( J tX K ) = U. ( J tX K )
73 eqid 
 |-  ( z e. U. ( J tX K ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) = ( z e. U. ( J tX K ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. )
74 72 73 txcnmpt 
 |-  ( ( ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) /\ ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) ) -> ( z e. U. ( J tX K ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
75 3 4 74 syl2anc 
 |-  ( ph -> ( z e. U. ( J tX K ) |-> <. ( ( x e. X , y e. Y |-> A ) ` z ) , ( ( x e. X , y e. Y |-> B ) ` z ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
76 71 75 eqeltrrd 
 |-  ( ph -> ( x e. X , y e. Y |-> <. A , B >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )