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