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