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