# 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 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
cnmpt2k.k ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({Y}\right)$
cnmpt2k.a ${⊢}{\phi }\to \left({x}\in {X},{y}\in {Y}⟼{A}\right)\in \left(\left({J}{×}_{t}{K}\right)\mathrm{Cn}{L}\right)$
Assertion cnmpt2k ${⊢}{\phi }\to \left({x}\in {X}⟼\left({y}\in {Y}⟼{A}\right)\right)\in \left({J}\mathrm{Cn}\left({L}{^}_{\mathrm{ko}}{K}\right)\right)$

### Proof

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