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 φ J TopOn X
cnmpt2k.k φ K TopOn Y
cnmpt2k.a φ x X , y Y A J × t K Cn L
Assertion cnmpt2k φ x X y Y A J Cn L ^ ko K

Proof

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