Metamath Proof Explorer

Theorem cnmptkk

Description: The composition of two curried functions is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmptkk.j 
|- ( ph -> J e. ( TopOn ` X ) )
cnmptkk.k 
|- ( ph -> K e. ( TopOn ` Y ) )
cnmptkk.l 
|- ( ph -> L e. ( TopOn ` Z ) )
cnmptkk.m 
|- ( ph -> M e. ( TopOn ` W ) )
cnmptkk.n 
|- ( ph -> L e. N-Locally Comp )
cnmptkk.a 
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
cnmptkk.b 
|- ( ph -> ( x e. X |-> ( z e. Z |-> B ) ) e. ( J Cn ( M ^ko L ) ) )
cnmptkk.c 
|- ( z = A -> B = C )
Assertion cnmptkk 
|- ( ph -> ( x e. X |-> ( y e. Y |-> C ) ) e. ( J Cn ( M ^ko K ) ) )

Proof

Step Hyp Ref Expression
1 cnmptkk.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmptkk.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 cnmptkk.l 
 |-  ( ph -> L e. ( TopOn ` Z ) )
4 cnmptkk.m 
 |-  ( ph -> M e. ( TopOn ` W ) )
5 cnmptkk.n 
 |-  ( ph -> L e. N-Locally Comp )
6 cnmptkk.a 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
7 cnmptkk.b 
 |-  ( ph -> ( x e. X |-> ( z e. Z |-> B ) ) e. ( J Cn ( M ^ko L ) ) )
8 cnmptkk.c 
 |-  ( z = A -> B = C )
9 2 adantr 
 |-  ( ( ph /\ x e. X ) -> K e. ( TopOn ` Y ) )
10 3 adantr 
 |-  ( ( ph /\ x e. X ) -> L e. ( TopOn ` Z ) )
11 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
12 2 11 syl 
 |-  ( ph -> K e. Top )
13 nllytop 
 |-  ( L e. N-Locally Comp -> L e. Top )
14 5 13 syl 
 |-  ( ph -> L e. Top )
15 eqid 
 |-  ( L ^ko K ) = ( L ^ko K )
16 15 xkotopon 
 |-  ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
17 12 14 16 syl2anc 
 |-  ( ph -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
18 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) /\ ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) ) -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) )
19 1 17 6 18 syl3anc 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) )
20 19 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) e. ( K Cn L ) )
21 cnf2 
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` Z ) /\ ( y e. Y |-> A ) e. ( K Cn L ) ) -> ( y e. Y |-> A ) : Y --> Z )
22 9 10 20 21 syl3anc 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) : Y --> Z )
23 eqid 
 |-  ( y e. Y |-> A ) = ( y e. Y |-> A )
24 23 fmpt 
 |-  ( A. y e. Y A e. Z <-> ( y e. Y |-> A ) : Y --> Z )
25 22 24 sylibr 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y A e. Z )
26 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) = ( y e. Y |-> A ) )
27 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( z e. Z |-> B ) = ( z e. Z |-> B ) )
28 25 26 27 8 fmptcof 
 |-  ( ( ph /\ x e. X ) -> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) = ( y e. Y |-> C ) )
29 28 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) ) = ( x e. X |-> ( y e. Y |-> C ) ) )
30 topontop 
 |-  ( M e. ( TopOn ` W ) -> M e. Top )
31 4 30 syl 
 |-  ( ph -> M e. Top )
32 eqid 
 |-  ( M ^ko L ) = ( M ^ko L )
33 32 xkotopon 
 |-  ( ( L e. Top /\ M e. Top ) -> ( M ^ko L ) e. ( TopOn ` ( L Cn M ) ) )
34 14 31 33 syl2anc 
 |-  ( ph -> ( M ^ko L ) e. ( TopOn ` ( L Cn M ) ) )
35 eqid 
 |-  ( f e. ( L Cn M ) , g e. ( K Cn L ) |-> ( f o. g ) ) = ( f e. ( L Cn M ) , g e. ( K Cn L ) |-> ( f o. g ) )
36 35 xkococn 
 |-  ( ( K e. Top /\ L e. N-Locally Comp /\ M e. Top ) -> ( f e. ( L Cn M ) , g e. ( K Cn L ) |-> ( f o. g ) ) e. ( ( ( M ^ko L ) tX ( L ^ko K ) ) Cn ( M ^ko K ) ) )
37 12 5 31 36 syl3anc 
 |-  ( ph -> ( f e. ( L Cn M ) , g e. ( K Cn L ) |-> ( f o. g ) ) e. ( ( ( M ^ko L ) tX ( L ^ko K ) ) Cn ( M ^ko K ) ) )
38 coeq1 
 |-  ( f = ( z e. Z |-> B ) -> ( f o. g ) = ( ( z e. Z |-> B ) o. g ) )
39 coeq2 
 |-  ( g = ( y e. Y |-> A ) -> ( ( z e. Z |-> B ) o. g ) = ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) )
40 38 39 sylan9eq 
 |-  ( ( f = ( z e. Z |-> B ) /\ g = ( y e. Y |-> A ) ) -> ( f o. g ) = ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) )
41 1 7 6 34 17 37 40 cnmpt12 
 |-  ( ph -> ( x e. X |-> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) ) e. ( J Cn ( M ^ko K ) ) )
42 29 41 eqeltrrd 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> C ) ) e. ( J Cn ( M ^ko K ) ) )