Metamath Proof Explorer

Theorem cnmpt12

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 12-Jun-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 ) )
cnmpt12.k 
|- ( ph -> K e. ( TopOn ` Y ) )
cnmpt12.l 
|- ( ph -> L e. ( TopOn ` Z ) )
cnmpt12.c 
|- ( ph -> ( y e. Y , z e. Z |-> C ) e. ( ( K tX L ) Cn M ) )
cnmpt12.d 
|- ( ( y = A /\ z = B ) -> C = D )
Assertion cnmpt12 
|- ( ph -> ( x e. X |-> D ) e. ( J Cn M ) )

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 cnmpt12.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
5 cnmpt12.l 
 |-  ( ph -> L e. ( TopOn ` Z ) )
6 cnmpt12.c 
 |-  ( ph -> ( y e. Y , z e. Z |-> C ) e. ( ( K tX L ) Cn M ) )
7 cnmpt12.d 
 |-  ( ( y = A /\ z = B ) -> C = D )
8 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ ( x e. X |-> A ) e. ( J Cn K ) ) -> ( x e. X |-> A ) : X --> Y )
9 1 4 2 8 syl3anc 
 |-  ( ph -> ( x e. X |-> A ) : X --> Y )
10 9 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> A e. Y )
11 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( TopOn ` Z ) /\ ( x e. X |-> B ) e. ( J Cn L ) ) -> ( x e. X |-> B ) : X --> Z )
12 1 5 3 11 syl3anc 
 |-  ( ph -> ( x e. X |-> B ) : X --> Z )
13 12 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> B e. Z )
14 10 13 jca 
 |-  ( ( ph /\ x e. X ) -> ( A e. Y /\ B e. Z ) )
15 txtopon 
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` Z ) ) -> ( K tX L ) e. ( TopOn ` ( Y X. Z ) ) )
16 4 5 15 syl2anc 
 |-  ( ph -> ( K tX L ) e. ( TopOn ` ( Y X. Z ) ) )
17 cntop2 
 |-  ( ( y e. Y , z e. Z |-> C ) e. ( ( K tX L ) Cn M ) -> M e. Top )
18 6 17 syl 
 |-  ( ph -> M e. Top )
19 toptopon2 
 |-  ( M e. Top <-> M e. ( TopOn ` U. M ) )
20 18 19 sylib 
 |-  ( ph -> M e. ( TopOn ` U. M ) )
21 cnf2 
 |-  ( ( ( K tX L ) e. ( TopOn ` ( Y X. Z ) ) /\ M e. ( TopOn ` U. M ) /\ ( y e. Y , z e. Z |-> C ) e. ( ( K tX L ) Cn M ) ) -> ( y e. Y , z e. Z |-> C ) : ( Y X. Z ) --> U. M )
22 16 20 6 21 syl3anc 
 |-  ( ph -> ( y e. Y , z e. Z |-> C ) : ( Y X. Z ) --> U. M )
23 eqid 
 |-  ( y e. Y , z e. Z |-> C ) = ( y e. Y , z e. Z |-> C )
24 23 fmpo 
 |-  ( A. y e. Y A. z e. Z C e. U. M <-> ( y e. Y , z e. Z |-> C ) : ( Y X. Z ) --> U. M )
25 22 24 sylibr 
 |-  ( ph -> A. y e. Y A. z e. Z C e. U. M )
26 r2al 
 |-  ( A. y e. Y A. z e. Z C e. U. M <-> A. y A. z ( ( y e. Y /\ z e. Z ) -> C e. U. M ) )
27 25 26 sylib 
 |-  ( ph -> A. y A. z ( ( y e. Y /\ z e. Z ) -> C e. U. M ) )
28 27 adantr 
 |-  ( ( ph /\ x e. X ) -> A. y A. z ( ( y e. Y /\ z e. Z ) -> C e. U. M ) )
29 eleq1 
 |-  ( y = A -> ( y e. Y <-> A e. Y ) )
30 eleq1 
 |-  ( z = B -> ( z e. Z <-> B e. Z ) )
31 29 30 bi2anan9 
 |-  ( ( y = A /\ z = B ) -> ( ( y e. Y /\ z e. Z ) <-> ( A e. Y /\ B e. Z ) ) )
32 7 eleq1d 
 |-  ( ( y = A /\ z = B ) -> ( C e. U. M <-> D e. U. M ) )
33 31 32 imbi12d 
 |-  ( ( y = A /\ z = B ) -> ( ( ( y e. Y /\ z e. Z ) -> C e. U. M ) <-> ( ( A e. Y /\ B e. Z ) -> D e. U. M ) ) )
34 33 spc2gv 
 |-  ( ( A e. Y /\ B e. Z ) -> ( A. y A. z ( ( y e. Y /\ z e. Z ) -> C e. U. M ) -> ( ( A e. Y /\ B e. Z ) -> D e. U. M ) ) )
35 14 28 14 34 syl3c 
 |-  ( ( ph /\ x e. X ) -> D e. U. M )
36 7 23 ovmpoga 
 |-  ( ( A e. Y /\ B e. Z /\ D e. U. M ) -> ( A ( y e. Y , z e. Z |-> C ) B ) = D )
37 10 13 35 36 syl3anc 
 |-  ( ( ph /\ x e. X ) -> ( A ( y e. Y , z e. Z |-> C ) B ) = D )
38 37 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( A ( y e. Y , z e. Z |-> C ) B ) ) = ( x e. X |-> D ) )
39 1 2 3 6 cnmpt12f 
 |-  ( ph -> ( x e. X |-> ( A ( y e. Y , z e. Z |-> C ) B ) ) e. ( J Cn M ) )
40 38 39 eqeltrrd 
 |-  ( ph -> ( x e. X |-> D ) e. ( J Cn M ) )