Metamath Proof Explorer

Theorem cnmpt2k

Description: The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypotheses cnmpt2k.j 
|- ( ph -> J e. ( TopOn ` X ) )
cnmpt2k.k 
|- ( ph -> K e. ( TopOn ` Y ) )
cnmpt2k.a 
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
Assertion cnmpt2k 
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )

Proof

Step Hyp Ref Expression
1 cnmpt2k.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmpt2k.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 cnmpt2k.a 
 |-  ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
4 nfcv 
 |-  F/_ x Y
5 nfcv 
 |-  F/_ x v
6 nfmpo2 
 |-  F/_ x ( y e. Y , x e. X |-> A )
7 nfcv 
 |-  F/_ x w
8 5 6 7 nfov 
 |-  F/_ x ( v ( y e. Y , x e. X |-> A ) w )
9 4 8 nfmpt 
 |-  F/_ x ( v e. Y |-> ( v ( y e. Y , x e. X |-> A ) w ) )
10 nfcv 
 |-  F/_ w ( y e. Y |-> ( y ( y e. Y , x e. X |-> A ) x ) )
11 nfcv 
 |-  F/_ y v
12 nfmpo1 
 |-  F/_ y ( y e. Y , x e. X |-> A )
13 nfcv 
 |-  F/_ y w
14 11 12 13 nfov 
 |-  F/_ y ( v ( y e. Y , x e. X |-> A ) w )
15 nfcv 
 |-  F/_ v ( y ( y e. Y , x e. X |-> A ) w )
16 oveq1 
 |-  ( v = y -> ( v ( y e. Y , x e. X |-> A ) w ) = ( y ( y e. Y , x e. X |-> A ) w ) )
17 14 15 16 cbvmpt 
 |-  ( v e. Y |-> ( v ( y e. Y , x e. X |-> A ) w ) ) = ( y e. Y |-> ( y ( y e. Y , x e. X |-> A ) w ) )
18 oveq2 
 |-  ( w = x -> ( y ( y e. Y , x e. X |-> A ) w ) = ( y ( y e. Y , x e. X |-> A ) x ) )
19 18 mpteq2dv 
 |-  ( w = x -> ( y e. Y |-> ( y ( y e. Y , x e. X |-> A ) w ) ) = ( y e. Y |-> ( y ( y e. Y , x e. X |-> A ) x ) ) )
20 17 19 eqtrid 
 |-  ( w = x -> ( v e. Y |-> ( v ( y e. Y , x e. X |-> A ) w ) ) = ( y e. Y |-> ( y ( y e. Y , x e. X |-> A ) x ) ) )
21 9 10 20 cbvmpt 
 |-  ( w e. X |-> ( v e. Y |-> ( v ( y e. Y , x e. X |-> A ) w ) ) ) = ( x e. X |-> ( y e. Y |-> ( y ( y e. Y , x e. X |-> A ) x ) ) )
22 simpr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> y e. Y )
23 simplr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> x e. X )
24 txtopon 
 |-  ( ( K e. ( TopOn ` Y ) /\ J e. ( TopOn ` X ) ) -> ( K tX J ) e. ( TopOn ` ( Y X. X ) ) )
25 2 1 24 syl2anc 
 |-  ( ph -> ( K tX J ) e. ( TopOn ` ( Y X. X ) ) )
26 cntop2 
 |-  ( ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) -> L e. Top )
27 3 26 syl 
 |-  ( ph -> L e. Top )
28 toptopon2 
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
29 27 28 sylib 
 |-  ( ph -> L e. ( TopOn ` U. L ) )
30 1 2 3 cnmptcom 
 |-  ( ph -> ( y e. Y , x e. X |-> A ) e. ( ( K tX J ) Cn L ) )
31 cnf2 
 |-  ( ( ( K tX J ) e. ( TopOn ` ( Y X. X ) ) /\ L e. ( TopOn ` U. L ) /\ ( y e. Y , x e. X |-> A ) e. ( ( K tX J ) Cn L ) ) -> ( y e. Y , x e. X |-> A ) : ( Y X. X ) --> U. L )
32 25 29 30 31 syl3anc 
 |-  ( ph -> ( y e. Y , x e. X |-> A ) : ( Y X. X ) --> U. L )
33 eqid 
 |-  ( y e. Y , x e. X |-> A ) = ( y e. Y , x e. X |-> A )
34 33 fmpo 
 |-  ( A. y e. Y A. x e. X A e. U. L <-> ( y e. Y , x e. X |-> A ) : ( Y X. X ) --> U. L )
35 32 34 sylibr 
 |-  ( ph -> A. y e. Y A. x e. X A e. U. L )
36 35 r19.21bi 
 |-  ( ( ph /\ y e. Y ) -> A. x e. X A e. U. L )
37 36 r19.21bi 
 |-  ( ( ( ph /\ y e. Y ) /\ x e. X ) -> A e. U. L )
38 37 an32s 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> A e. U. L )
39 33 ovmpt4g 
 |-  ( ( y e. Y /\ x e. X /\ A e. U. L ) -> ( y ( y e. Y , x e. X |-> A ) x ) = A )
40 22 23 38 39 syl3anc 
 |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> ( y ( y e. Y , x e. X |-> A ) x ) = A )
41 40 mpteq2dva 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> ( y ( y e. Y , x e. X |-> A ) x ) ) = ( y e. Y |-> A ) )
42 41 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> ( y ( y e. Y , x e. X |-> A ) x ) ) ) = ( x e. X |-> ( y e. Y |-> A ) ) )
43 21 42 eqtrid 
 |-  ( ph -> ( w e. X |-> ( v e. Y |-> ( v ( y e. Y , x e. X |-> A ) w ) ) ) = ( x e. X |-> ( y e. Y |-> A ) ) )
44 eqid 
 |-  ( w e. X |-> ( v e. Y |-> <. v , w >. ) ) = ( w e. X |-> ( v e. Y |-> <. v , w >. ) )
45 44 xkoinjcn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( w e. X |-> ( v e. Y |-> <. v , w >. ) ) e. ( J Cn ( ( K tX J ) ^ko K ) ) )
46 1 2 45 syl2anc 
 |-  ( ph -> ( w e. X |-> ( v e. Y |-> <. v , w >. ) ) e. ( J Cn ( ( K tX J ) ^ko K ) ) )
47 32 feqmptd 
 |-  ( ph -> ( y e. Y , x e. X |-> A ) = ( z e. ( Y X. X ) |-> ( ( y e. Y , x e. X |-> A ) ` z ) ) )
48 47 30 eqeltrrd 
 |-  ( ph -> ( z e. ( Y X. X ) |-> ( ( y e. Y , x e. X |-> A ) ` z ) ) e. ( ( K tX J ) Cn L ) )
49 fveq2 
 |-  ( z = <. v , w >. -> ( ( y e. Y , x e. X |-> A ) ` z ) = ( ( y e. Y , x e. X |-> A ) ` <. v , w >. ) )
50 df-ov 
 |-  ( v ( y e. Y , x e. X |-> A ) w ) = ( ( y e. Y , x e. X |-> A ) ` <. v , w >. )
51 49 50 eqtr4di 
 |-  ( z = <. v , w >. -> ( ( y e. Y , x e. X |-> A ) ` z ) = ( v ( y e. Y , x e. X |-> A ) w ) )
52 1 2 25 46 48 51 cnmptk1 
 |-  ( ph -> ( w e. X |-> ( v e. Y |-> ( v ( y e. Y , x e. X |-> A ) w ) ) ) e. ( J Cn ( L ^ko K ) ) )
53 43 52 eqeltrrd 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )