Metamath Proof Explorer


Theorem cnmptk1p

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

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

Proof

Step Hyp Ref Expression
1 cnmptk1p.j
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmptk1p.k
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 cnmptk1p.l
 |-  ( ph -> L e. ( TopOn ` Z ) )
4 cnmptk1p.n
 |-  ( ph -> K e. N-Locally Comp )
5 cnmptk1p.a
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
6 cnmptk1p.b
 |-  ( ph -> ( x e. X |-> B ) e. ( J Cn K ) )
7 cnmptk1p.c
 |-  ( y = B -> A = C )
8 eqid
 |-  ( y e. Y |-> A ) = ( y e. Y |-> A )
9 cnf2
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ ( x e. X |-> B ) e. ( J Cn K ) ) -> ( x e. X |-> B ) : X --> Y )
10 1 2 6 9 syl3anc
 |-  ( ph -> ( x e. X |-> B ) : X --> Y )
11 10 fvmptelrn
 |-  ( ( ph /\ x e. X ) -> B e. Y )
12 7 eleq1d
 |-  ( y = B -> ( A e. Z <-> C e. Z ) )
13 2 adantr
 |-  ( ( ph /\ x e. X ) -> K e. ( TopOn ` Y ) )
14 3 adantr
 |-  ( ( ph /\ x e. X ) -> L e. ( TopOn ` Z ) )
15 nllytop
 |-  ( K e. N-Locally Comp -> K e. Top )
16 4 15 syl
 |-  ( ph -> K e. Top )
17 topontop
 |-  ( L e. ( TopOn ` Z ) -> L e. Top )
18 3 17 syl
 |-  ( ph -> L e. Top )
19 eqid
 |-  ( L ^ko K ) = ( L ^ko K )
20 19 xkotopon
 |-  ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
21 16 18 20 syl2anc
 |-  ( ph -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
22 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 ) )
23 1 21 5 22 syl3anc
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) )
24 23 fvmptelrn
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) e. ( K Cn L ) )
25 cnf2
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` Z ) /\ ( y e. Y |-> A ) e. ( K Cn L ) ) -> ( y e. Y |-> A ) : Y --> Z )
26 13 14 24 25 syl3anc
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) : Y --> Z )
27 8 fmpt
 |-  ( A. y e. Y A e. Z <-> ( y e. Y |-> A ) : Y --> Z )
28 26 27 sylibr
 |-  ( ( ph /\ x e. X ) -> A. y e. Y A e. Z )
29 12 28 11 rspcdva
 |-  ( ( ph /\ x e. X ) -> C e. Z )
30 8 7 11 29 fvmptd3
 |-  ( ( ph /\ x e. X ) -> ( ( y e. Y |-> A ) ` B ) = C )
31 30 mpteq2dva
 |-  ( ph -> ( x e. X |-> ( ( y e. Y |-> A ) ` B ) ) = ( x e. X |-> C ) )
32 eqid
 |-  ( K Cn L ) = ( K Cn L )
33 toponuni
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
34 2 33 syl
 |-  ( ph -> Y = U. K )
35 mpoeq12
 |-  ( ( ( K Cn L ) = ( K Cn L ) /\ Y = U. K ) -> ( f e. ( K Cn L ) , z e. Y |-> ( f ` z ) ) = ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) )
36 32 34 35 sylancr
 |-  ( ph -> ( f e. ( K Cn L ) , z e. Y |-> ( f ` z ) ) = ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) )
37 eqid
 |-  U. K = U. K
38 eqid
 |-  ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) = ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) )
39 37 38 xkofvcn
 |-  ( ( K e. N-Locally Comp /\ L e. Top ) -> ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) e. ( ( ( L ^ko K ) tX K ) Cn L ) )
40 4 18 39 syl2anc
 |-  ( ph -> ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) e. ( ( ( L ^ko K ) tX K ) Cn L ) )
41 36 40 eqeltrd
 |-  ( ph -> ( f e. ( K Cn L ) , z e. Y |-> ( f ` z ) ) e. ( ( ( L ^ko K ) tX K ) Cn L ) )
42 fveq1
 |-  ( f = ( y e. Y |-> A ) -> ( f ` z ) = ( ( y e. Y |-> A ) ` z ) )
43 fveq2
 |-  ( z = B -> ( ( y e. Y |-> A ) ` z ) = ( ( y e. Y |-> A ) ` B ) )
44 42 43 sylan9eq
 |-  ( ( f = ( y e. Y |-> A ) /\ z = B ) -> ( f ` z ) = ( ( y e. Y |-> A ) ` B ) )
45 1 5 6 21 2 41 44 cnmpt12
 |-  ( ph -> ( x e. X |-> ( ( y e. Y |-> A ) ` B ) ) e. ( J Cn L ) )
46 31 45 eqeltrrd
 |-  ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )