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 | |
|
cnmptk1p.k | |
||
cnmptk1p.l | |
||
cnmptk1p.n | |
||
cnmptk1p.a | |
||
cnmptk1p.b | |
||
cnmptk1p.c | |
||
Assertion | cnmptk1p | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnmptk1p.j | |
|
2 | cnmptk1p.k | |
|
3 | cnmptk1p.l | |
|
4 | cnmptk1p.n | |
|
5 | cnmptk1p.a | |
|
6 | cnmptk1p.b | |
|
7 | cnmptk1p.c | |
|
8 | eqid | |
|
9 | cnf2 | |
|
10 | 1 2 6 9 | syl3anc | |
11 | 10 | fvmptelcdm | |
12 | 7 | eleq1d | |
13 | 2 | adantr | |
14 | 3 | adantr | |
15 | nllytop | |
|
16 | 4 15 | syl | |
17 | topontop | |
|
18 | 3 17 | syl | |
19 | eqid | |
|
20 | 19 | xkotopon | |
21 | 16 18 20 | syl2anc | |
22 | cnf2 | |
|
23 | 1 21 5 22 | syl3anc | |
24 | 23 | fvmptelcdm | |
25 | cnf2 | |
|
26 | 13 14 24 25 | syl3anc | |
27 | 8 | fmpt | |
28 | 26 27 | sylibr | |
29 | 12 28 11 | rspcdva | |
30 | 8 7 11 29 | fvmptd3 | |
31 | 30 | mpteq2dva | |
32 | eqid | |
|
33 | toponuni | |
|
34 | 2 33 | syl | |
35 | mpoeq12 | |
|
36 | 32 34 35 | sylancr | |
37 | eqid | |
|
38 | eqid | |
|
39 | 37 38 | xkofvcn | |
40 | 4 18 39 | syl2anc | |
41 | 36 40 | eqeltrd | |
42 | fveq1 | |
|
43 | fveq2 | |
|
44 | 42 43 | sylan9eq | |
45 | 1 5 6 21 2 41 44 | cnmpt12 | |
46 | 31 45 | eqeltrrd | |