Metamath Proof Explorer

Theorem cnmptk2

Description: The uncurrying of a curried function is 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 )
cnmptk2.a 
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
Assertion cnmptk2 
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) 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 cnmptk2.a 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
6 nffvmpt1 
 |-  F/_ x ( ( x e. X |-> ( y e. Y |-> A ) ) ` w )
7 nfcv 
 |-  F/_ x k
8 6 7 nffv 
 |-  F/_ x ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k )
9 nfcv 
 |-  F/_ y X
10 nfmpt1 
 |-  F/_ y ( y e. Y |-> A )
11 9 10 nfmpt 
 |-  F/_ y ( x e. X |-> ( y e. Y |-> A ) )
12 nfcv 
 |-  F/_ y w
13 11 12 nffv 
 |-  F/_ y ( ( x e. X |-> ( y e. Y |-> A ) ) ` w )
14 nfcv 
 |-  F/_ y k
15 13 14 nffv 
 |-  F/_ y ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k )
16 nfcv 
 |-  F/_ w ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y )
17 nfcv 
 |-  F/_ k ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y )
18 fveq2 
 |-  ( w = x -> ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) = ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) )
19 18 fveq1d 
 |-  ( w = x -> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k ) = ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` k ) )
20 fveq2 
 |-  ( k = y -> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` k ) = ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y ) )
21 19 20 sylan9eq 
 |-  ( ( w = x /\ k = y ) -> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k ) = ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y ) )
22 8 15 16 17 21 cbvmpo 
 |-  ( w e. X , k e. Y |-> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k ) ) = ( x e. X , y e. Y |-> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y ) )
23 simplr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> x e. X )
24 nllytop 
 |-  ( K e. N-Locally Comp -> K e. Top )
25 4 24 syl 
 |-  ( ph -> K e. Top )
26 topontop 
 |-  ( L e. ( TopOn ` Z ) -> L e. Top )
27 3 26 syl 
 |-  ( ph -> L e. Top )
28 eqid 
 |-  ( L ^ko K ) = ( L ^ko K )
29 28 xkotopon 
 |-  ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
30 25 27 29 syl2anc 
 |-  ( ph -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
31 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 ) )
32 1 30 5 31 syl3anc 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) )
33 32 fvmptelrn 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) e. ( K Cn L ) )
34 33 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( y e. Y |-> A ) e. ( K Cn L ) )
35 eqid 
 |-  ( x e. X |-> ( y e. Y |-> A ) ) = ( x e. X |-> ( y e. Y |-> A ) )
36 35 fvmpt2 
 |-  ( ( x e. X /\ ( y e. Y |-> A ) e. ( K Cn L ) ) -> ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) = ( y e. Y |-> A ) )
37 23 34 36 syl2anc 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) = ( y e. Y |-> A ) )
38 37 fveq1d 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y ) = ( ( y e. Y |-> A ) ` y ) )
39 simpr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> y e. Y )
40 2 adantr 
 |-  ( ( ph /\ x e. X ) -> K e. ( TopOn ` Y ) )
41 3 adantr 
 |-  ( ( ph /\ x e. X ) -> L e. ( TopOn ` Z ) )
42 cnf2 
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` Z ) /\ ( y e. Y |-> A ) e. ( K Cn L ) ) -> ( y e. Y |-> A ) : Y --> Z )
43 40 41 33 42 syl3anc 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) : Y --> Z )
44 43 fvmptelrn 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> A e. Z )
45 eqid 
 |-  ( y e. Y |-> A ) = ( y e. Y |-> A )
46 45 fvmpt2 
 |-  ( ( y e. Y /\ A e. Z ) -> ( ( y e. Y |-> A ) ` y ) = A )
47 39 44 46 syl2anc 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( ( y e. Y |-> A ) ` y ) = A )
48 38 47 eqtrd 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y ) = A )
49 48 3impa 
 |-  ( ( ph /\ x e. X /\ y e. Y ) -> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y ) = A )
50 49 mpoeq3dva 
 |-  ( ph -> ( x e. X , y e. Y |-> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` x ) ` y ) ) = ( x e. X , y e. Y |-> A ) )
51 22 50 eqtrid 
 |-  ( ph -> ( w e. X , k e. Y |-> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k ) ) = ( x e. X , y e. Y |-> A ) )
52 1 2 cnmpt1st 
 |-  ( ph -> ( w e. X , k e. Y |-> w ) e. ( ( J tX K ) Cn J ) )
53 1 2 52 5 cnmpt21f 
 |-  ( ph -> ( w e. X , k e. Y |-> ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ) e. ( ( J tX K ) Cn ( L ^ko K ) ) )
54 1 2 cnmpt2nd 
 |-  ( ph -> ( w e. X , k e. Y |-> k ) e. ( ( J tX K ) Cn K ) )
55 eqid 
 |-  ( K Cn L ) = ( K Cn L )
56 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
57 2 56 syl 
 |-  ( ph -> Y = U. K )
58 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 ) ) )
59 55 57 58 sylancr 
 |-  ( ph -> ( f e. ( K Cn L ) , z e. Y |-> ( f ` z ) ) = ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) )
60 eqid 
 |-  U. K = U. K
61 eqid 
 |-  ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) = ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) )
62 60 61 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 ) )
63 4 27 62 syl2anc 
 |-  ( ph -> ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) e. ( ( ( L ^ko K ) tX K ) Cn L ) )
64 59 63 eqeltrd 
 |-  ( ph -> ( f e. ( K Cn L ) , z e. Y |-> ( f ` z ) ) e. ( ( ( L ^ko K ) tX K ) Cn L ) )
65 fveq1 
 |-  ( f = ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) -> ( f ` z ) = ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` z ) )
66 fveq2 
 |-  ( z = k -> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` z ) = ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k ) )
67 65 66 sylan9eq 
 |-  ( ( f = ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) /\ z = k ) -> ( f ` z ) = ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k ) )
68 1 2 53 54 30 2 64 67 cnmpt22 
 |-  ( ph -> ( w e. X , k e. Y |-> ( ( ( x e. X |-> ( y e. Y |-> A ) ) ` w ) ` k ) ) e. ( ( J tX K ) Cn L ) )
69 51 68 eqeltrrd 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )