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 φJTopOnX
cnmptk1p.k φKTopOnY
cnmptk1p.l φLTopOnZ
cnmptk1p.n φKN-Locally Comp
cnmptk1p.a φxXyYAJCnL^koK
cnmptk1p.b φxXBJCnK
cnmptk1p.c y=BA=C
Assertion cnmptk1p φxXCJCnL

Proof

Step Hyp Ref Expression
1 cnmptk1p.j φJTopOnX
2 cnmptk1p.k φKTopOnY
3 cnmptk1p.l φLTopOnZ
4 cnmptk1p.n φKN-Locally Comp
5 cnmptk1p.a φxXyYAJCnL^koK
6 cnmptk1p.b φxXBJCnK
7 cnmptk1p.c y=BA=C
8 eqid yYA=yYA
9 cnf2 JTopOnXKTopOnYxXBJCnKxXB:XY
10 1 2 6 9 syl3anc φxXB:XY
11 10 fvmptelcdm φxXBY
12 7 eleq1d y=BAZCZ
13 2 adantr φxXKTopOnY
14 3 adantr φxXLTopOnZ
15 nllytop KN-Locally Comp KTop
16 4 15 syl φKTop
17 topontop LTopOnZLTop
18 3 17 syl φLTop
19 eqid L^koK=L^koK
20 19 xkotopon KTopLTopL^koKTopOnKCnL
21 16 18 20 syl2anc φL^koKTopOnKCnL
22 cnf2 JTopOnXL^koKTopOnKCnLxXyYAJCnL^koKxXyYA:XKCnL
23 1 21 5 22 syl3anc φxXyYA:XKCnL
24 23 fvmptelcdm φxXyYAKCnL
25 cnf2 KTopOnYLTopOnZyYAKCnLyYA:YZ
26 13 14 24 25 syl3anc φxXyYA:YZ
27 8 fmpt yYAZyYA:YZ
28 26 27 sylibr φxXyYAZ
29 12 28 11 rspcdva φxXCZ
30 8 7 11 29 fvmptd3 φxXyYAB=C
31 30 mpteq2dva φxXyYAB=xXC
32 eqid KCnL=KCnL
33 toponuni KTopOnYY=K
34 2 33 syl φY=K
35 mpoeq12 KCnL=KCnLY=KfKCnL,zYfz=fKCnL,zKfz
36 32 34 35 sylancr φfKCnL,zYfz=fKCnL,zKfz
37 eqid K=K
38 eqid fKCnL,zKfz=fKCnL,zKfz
39 37 38 xkofvcn KN-Locally Comp LTop fKCnL,zKfzL^koK×tKCnL
40 4 18 39 syl2anc φfKCnL,zKfzL^koK×tKCnL
41 36 40 eqeltrd φfKCnL,zYfzL^koK×tKCnL
42 fveq1 f=yYAfz=yYAz
43 fveq2 z=ByYAz=yYAB
44 42 43 sylan9eq f=yYAz=Bfz=yYAB
45 1 5 6 21 2 41 44 cnmpt12 φxXyYABJCnL
46 31 45 eqeltrrd φxXCJCnL