Metamath Proof Explorer

Theorem cnmpt21

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 ) )
cnmpt21.l 
|- ( ph -> L e. ( TopOn ` Z ) )
cnmpt21.b 
|- ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )
cnmpt21.c 
|- ( z = A -> B = C )
Assertion cnmpt21 
|- ( ph -> ( x e. X , y e. Y |-> C ) e. ( ( J tX K ) Cn 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 cnmpt21.l 
 |-  ( ph -> L e. ( TopOn ` Z ) )
5 cnmpt21.b 
 |-  ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )
6 cnmpt21.c 
 |-  ( z = A -> B = C )
7 df-ov 
 |-  ( x ( x e. X , y e. Y |-> A ) y ) = ( ( x e. X , y e. Y |-> A ) ` <. x , y >. )
8 simprl 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> x e. X )
9 simprr 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> y e. Y )
10 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
11 1 2 10 syl2anc 
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
12 cnf2 
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` Z ) /\ ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
13 11 4 3 12 syl3anc 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
14 eqid 
 |-  ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A )
15 14 fmpo 
 |-  ( A. x e. X A. y e. Y A e. Z <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
16 13 15 sylibr 
 |-  ( ph -> A. x e. X A. y e. Y A e. Z )
17 rsp2 
 |-  ( A. x e. X A. y e. Y A e. Z -> ( ( x e. X /\ y e. Y ) -> A e. Z ) )
18 16 17 syl 
 |-  ( ph -> ( ( x e. X /\ y e. Y ) -> A e. Z ) )
19 18 imp 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> A e. Z )
20 14 ovmpt4g 
 |-  ( ( x e. X /\ y e. Y /\ A e. Z ) -> ( x ( x e. X , y e. Y |-> A ) y ) = A )
21 8 9 19 20 syl3anc 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( x ( x e. X , y e. Y |-> A ) y ) = A )
22 7 21 syl5eqr 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) = A )
23 22 fveq2d 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( z e. Z |-> B ) ` ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) ) = ( ( z e. Z |-> B ) ` A ) )
24 eqid 
 |-  ( z e. Z |-> B ) = ( z e. Z |-> B )
25 6 eleq1d 
 |-  ( z = A -> ( B e. U. M <-> C e. U. M ) )
26 cntop2 
 |-  ( ( z e. Z |-> B ) e. ( L Cn M ) -> M e. Top )
27 5 26 syl 
 |-  ( ph -> M e. Top )
28 toptopon2 
 |-  ( M e. Top <-> M e. ( TopOn ` U. M ) )
29 27 28 sylib 
 |-  ( ph -> M e. ( TopOn ` U. M ) )
30 cnf2 
 |-  ( ( L e. ( TopOn ` Z ) /\ M e. ( TopOn ` U. M ) /\ ( z e. Z |-> B ) e. ( L Cn M ) ) -> ( z e. Z |-> B ) : Z --> U. M )
31 4 29 5 30 syl3anc 
 |-  ( ph -> ( z e. Z |-> B ) : Z --> U. M )
32 24 fmpt 
 |-  ( A. z e. Z B e. U. M <-> ( z e. Z |-> B ) : Z --> U. M )
33 31 32 sylibr 
 |-  ( ph -> A. z e. Z B e. U. M )
34 33 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> A. z e. Z B e. U. M )
35 25 34 19 rspcdva 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> C e. U. M )
36 24 6 19 35 fvmptd3 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( z e. Z |-> B ) ` A ) = C )
37 23 36 eqtrd 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( z e. Z |-> B ) ` ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) ) = C )
38 opelxpi 
 |-  ( ( x e. X /\ y e. Y ) -> <. x , y >. e. ( X X. Y ) )
39 fvco3 
 |-  ( ( ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z /\ <. x , y >. e. ( X X. Y ) ) -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( z e. Z |-> B ) ` ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) ) )
40 13 38 39 syl2an 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( z e. Z |-> B ) ` ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) ) )
41 df-ov 
 |-  ( x ( x e. X , y e. Y |-> C ) y ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. )
42 eqid 
 |-  ( x e. X , y e. Y |-> C ) = ( x e. X , y e. Y |-> C )
43 42 ovmpt4g 
 |-  ( ( x e. X /\ y e. Y /\ C e. U. M ) -> ( x ( x e. X , y e. Y |-> C ) y ) = C )
44 8 9 35 43 syl3anc 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( x ( x e. X , y e. Y |-> C ) y ) = C )
45 41 44 syl5eqr 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) = C )
46 37 40 45 3eqtr4d 
 |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) )
47 46 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) )
48 nfv 
 |-  F/ u A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. )
49 nfcv 
 |-  F/_ x Y
50 nfcv 
 |-  F/_ x ( z e. Z |-> B )
51 nfmpo1 
 |-  F/_ x ( x e. X , y e. Y |-> A )
52 50 51 nfco 
 |-  F/_ x ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) )
53 nfcv 
 |-  F/_ x <. u , v >.
54 52 53 nffv 
 |-  F/_ x ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. )
55 nfmpo1 
 |-  F/_ x ( x e. X , y e. Y |-> C )
56 55 53 nffv 
 |-  F/_ x ( ( x e. X , y e. Y |-> C ) ` <. u , v >. )
57 54 56 nfeq 
 |-  F/ x ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. )
58 49 57 nfralw 
 |-  F/ x A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. )
59 nfv 
 |-  F/ v ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. )
60 nfcv 
 |-  F/_ y ( z e. Z |-> B )
61 nfmpo2 
 |-  F/_ y ( x e. X , y e. Y |-> A )
62 60 61 nfco 
 |-  F/_ y ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) )
63 nfcv 
 |-  F/_ y <. x , v >.
64 62 63 nffv 
 |-  F/_ y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. )
65 nfmpo2 
 |-  F/_ y ( x e. X , y e. Y |-> C )
66 65 63 nffv 
 |-  F/_ y ( ( x e. X , y e. Y |-> C ) ` <. x , v >. )
67 64 66 nfeq 
 |-  F/ y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. )
68 opeq2 
 |-  ( y = v -> <. x , y >. = <. x , v >. )
69 68 fveq2d 
 |-  ( y = v -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) )
70 68 fveq2d 
 |-  ( y = v -> ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) )
71 69 70 eqeq12d 
 |-  ( y = v -> ( ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) <-> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) ) )
72 59 67 71 cbvralw 
 |-  ( A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) <-> A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) )
73 opeq1 
 |-  ( x = u -> <. x , v >. = <. u , v >. )
74 73 fveq2d 
 |-  ( x = u -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) )
75 73 fveq2d 
 |-  ( x = u -> ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
76 74 75 eqeq12d 
 |-  ( x = u -> ( ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) <-> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) ) )
77 76 ralbidv 
 |-  ( x = u -> ( A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) <-> A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) ) )
78 72 77 syl5bb 
 |-  ( x = u -> ( A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) <-> A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) ) )
79 48 58 78 cbvralw 
 |-  ( A. x e. X A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) <-> A. u e. X A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
80 47 79 sylib 
 |-  ( ph -> A. u e. X A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
81 fveq2 
 |-  ( w = <. u , v >. -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) )
82 fveq2 
 |-  ( w = <. u , v >. -> ( ( x e. X , y e. Y |-> C ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
83 81 82 eqeq12d 
 |-  ( w = <. u , v >. -> ( ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) <-> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) ) )
84 83 ralxp 
 |-  ( A. w e. ( X X. Y ) ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) <-> A. u e. X A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
85 80 84 sylibr 
 |-  ( ph -> A. w e. ( X X. Y ) ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) )
86 fco 
 |-  ( ( ( z e. Z |-> B ) : Z --> U. M /\ ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z ) -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) : ( X X. Y ) --> U. M )
87 31 13 86 syl2anc 
 |-  ( ph -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) : ( X X. Y ) --> U. M )
88 87 ffnd 
 |-  ( ph -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) Fn ( X X. Y ) )
89 35 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. Y C e. U. M )
90 42 fmpo 
 |-  ( A. x e. X A. y e. Y C e. U. M <-> ( x e. X , y e. Y |-> C ) : ( X X. Y ) --> U. M )
91 89 90 sylib 
 |-  ( ph -> ( x e. X , y e. Y |-> C ) : ( X X. Y ) --> U. M )
92 91 ffnd 
 |-  ( ph -> ( x e. X , y e. Y |-> C ) Fn ( X X. Y ) )
93 eqfnfv 
 |-  ( ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) Fn ( X X. Y ) /\ ( x e. X , y e. Y |-> C ) Fn ( X X. Y ) ) -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) = ( x e. X , y e. Y |-> C ) <-> A. w e. ( X X. Y ) ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) ) )
94 88 92 93 syl2anc 
 |-  ( ph -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) = ( x e. X , y e. Y |-> C ) <-> A. w e. ( X X. Y ) ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) ) )
95 85 94 mpbird 
 |-  ( ph -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) = ( x e. X , y e. Y |-> C ) )
96 cnco 
 |-  ( ( ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) /\ ( z e. Z |-> B ) e. ( L Cn M ) ) -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) e. ( ( J tX K ) Cn M ) )
97 3 5 96 syl2anc 
 |-  ( ph -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) e. ( ( J tX K ) Cn M ) )
98 95 97 eqeltrrd 
 |-  ( ph -> ( x e. X , y e. Y |-> C ) e. ( ( J tX K ) Cn M ) )