Metamath Proof Explorer

Theorem cnmptk1

Description: The composition of a curried function with a one-arg function is continuous. (Contributed by Mario Carneiro, 23-Mar-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 ) )
cnmptk1.a 
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
cnmptk1.b 
|- ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )
cnmptk1.c 
|- ( z = A -> B = C )
Assertion cnmptk1 
|- ( ph -> ( x e. X |-> ( y e. Y |-> C ) ) e. ( J Cn ( M ^ko K ) ) )

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 cnmptk1.a 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
5 cnmptk1.b 
 |-  ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )
6 cnmptk1.c 
 |-  ( z = A -> B = C )
7 2 adantr 
 |-  ( ( ph /\ x e. X ) -> K e. ( TopOn ` Y ) )
8 3 adantr 
 |-  ( ( ph /\ x e. X ) -> L e. ( TopOn ` Z ) )
9 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
10 2 9 syl 
 |-  ( ph -> K e. Top )
11 topontop 
 |-  ( L e. ( TopOn ` Z ) -> L e. Top )
12 3 11 syl 
 |-  ( ph -> L e. Top )
13 eqid 
 |-  ( L ^ko K ) = ( L ^ko K )
14 13 xkotopon 
 |-  ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
15 10 12 14 syl2anc 
 |-  ( ph -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
16 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 ) )
17 1 15 4 16 syl3anc 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) )
18 17 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) e. ( K Cn L ) )
19 cnf2 
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` Z ) /\ ( y e. Y |-> A ) e. ( K Cn L ) ) -> ( y e. Y |-> A ) : Y --> Z )
20 7 8 18 19 syl3anc 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) : Y --> Z )
21 eqid 
 |-  ( y e. Y |-> A ) = ( y e. Y |-> A )
22 21 fmpt 
 |-  ( A. y e. Y A e. Z <-> ( y e. Y |-> A ) : Y --> Z )
23 20 22 sylibr 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y A e. Z )
24 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) = ( y e. Y |-> A ) )
25 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( z e. Z |-> B ) = ( z e. Z |-> B ) )
26 23 24 25 6 fmptcof 
 |-  ( ( ph /\ x e. X ) -> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) = ( y e. Y |-> C ) )
27 26 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) ) = ( x e. X |-> ( y e. Y |-> C ) ) )
28 10 5 xkoco2cn 
 |-  ( ph -> ( w e. ( K Cn L ) |-> ( ( z e. Z |-> B ) o. w ) ) e. ( ( L ^ko K ) Cn ( M ^ko K ) ) )
29 coeq2 
 |-  ( w = ( y e. Y |-> A ) -> ( ( z e. Z |-> B ) o. w ) = ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) )
30 1 4 15 28 29 cnmpt11 
 |-  ( ph -> ( x e. X |-> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) ) e. ( J Cn ( M ^ko K ) ) )
31 27 30 eqeltrrd 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> C ) ) e. ( J Cn ( M ^ko K ) ) )