Metamath Proof Explorer

Theorem cnmpt1k

Description: The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 cnmptk1.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmptk1.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 cnmptk1.l 
 |-  ( ph -> L e. ( TopOn ` Z ) )
4 cnmpt1k.m 
 |-  ( ph -> M e. ( TopOn ` W ) )
5 cnmpt1k.a 
 |-  ( ph -> ( x e. X |-> A ) e. ( J Cn L ) )
6 cnmpt1k.b 
 |-  ( ph -> ( y e. Y |-> ( z e. Z |-> B ) ) e. ( K Cn ( M ^ko L ) ) )
7 cnmpt1k.c 
 |-  ( z = A -> B = C )
8 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( TopOn ` Z ) /\ ( x e. X |-> A ) e. ( J Cn L ) ) -> ( x e. X |-> A ) : X --> Z )
9 1 3 5 8 syl3anc 
 |-  ( ph -> ( x e. X |-> A ) : X --> Z )
10 eqid 
 |-  ( x e. X |-> A ) = ( x e. X |-> A )
11 10 fmpt 
 |-  ( A. x e. X A e. Z <-> ( x e. X |-> A ) : X --> Z )
12 9 11 sylibr 
 |-  ( ph -> A. x e. X A e. Z )
13 12 adantr 
 |-  ( ( ph /\ y e. Y ) -> A. x e. X A e. Z )
14 eqidd 
 |-  ( ( ph /\ y e. Y ) -> ( x e. X |-> A ) = ( x e. X |-> A ) )
15 eqidd 
 |-  ( ( ph /\ y e. Y ) -> ( z e. Z |-> B ) = ( z e. Z |-> B ) )
16 13 14 15 7 fmptcof 
 |-  ( ( ph /\ y e. Y ) -> ( ( z e. Z |-> B ) o. ( x e. X |-> A ) ) = ( x e. X |-> C ) )
17 16 mpteq2dva 
 |-  ( ph -> ( y e. Y |-> ( ( z e. Z |-> B ) o. ( x e. X |-> A ) ) ) = ( y e. Y |-> ( x e. X |-> C ) ) )
18 topontop 
 |-  ( L e. ( TopOn ` Z ) -> L e. Top )
19 3 18 syl 
 |-  ( ph -> L e. Top )
20 topontop 
 |-  ( M e. ( TopOn ` W ) -> M e. Top )
21 4 20 syl 
 |-  ( ph -> M e. Top )
22 eqid 
 |-  ( M ^ko L ) = ( M ^ko L )
23 22 xkotopon 
 |-  ( ( L e. Top /\ M e. Top ) -> ( M ^ko L ) e. ( TopOn ` ( L Cn M ) ) )
24 19 21 23 syl2anc 
 |-  ( ph -> ( M ^ko L ) e. ( TopOn ` ( L Cn M ) ) )
25 21 5 xkoco1cn 
 |-  ( ph -> ( w e. ( L Cn M ) |-> ( w o. ( x e. X |-> A ) ) ) e. ( ( M ^ko L ) Cn ( M ^ko J ) ) )
26 coeq1 
 |-  ( w = ( z e. Z |-> B ) -> ( w o. ( x e. X |-> A ) ) = ( ( z e. Z |-> B ) o. ( x e. X |-> A ) ) )
27 2 6 24 25 26 cnmpt11 
 |-  ( ph -> ( y e. Y |-> ( ( z e. Z |-> B ) o. ( x e. X |-> A ) ) ) e. ( K Cn ( M ^ko J ) ) )
28 17 27 eqeltrrd 
 |-  ( ph -> ( y e. Y |-> ( x e. X |-> C ) ) e. ( K Cn ( M ^ko J ) ) )