# Metamath Proof Explorer

## Theorem curry2

Description: Composition with  ' ( 1st |( _V X. { C } ) ) turns any binary operation F with a constant second operand into a function G of the first operand only. This transformation is called "currying." (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis curry2.1 ${⊢}{G}={F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}$
Assertion curry2 ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to {G}=\left({x}\in {A}⟼{x}{F}{C}\right)$

### Proof

Step Hyp Ref Expression
1 curry2.1 ${⊢}{G}={F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}$
2 fnfun ${⊢}{F}Fn\left({A}×{B}\right)\to \mathrm{Fun}{F}$
3 1stconst ${⊢}{C}\in {B}\to \left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right):\mathrm{V}×\left\{{C}\right\}\underset{1-1 onto}{⟶}\mathrm{V}$
4 dff1o3 ${⊢}\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right):\mathrm{V}×\left\{{C}\right\}\underset{1-1 onto}{⟶}\mathrm{V}↔\left(\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right):\mathrm{V}×\left\{{C}\right\}\underset{onto}{⟶}\mathrm{V}\wedge \mathrm{Fun}{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)$
5 4 simprbi ${⊢}\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right):\mathrm{V}×\left\{{C}\right\}\underset{1-1 onto}{⟶}\mathrm{V}\to \mathrm{Fun}{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}$
6 3 5 syl ${⊢}{C}\in {B}\to \mathrm{Fun}{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}$
7 funco ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)\to \mathrm{Fun}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)$
8 2 6 7 syl2an ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to \mathrm{Fun}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)$
9 dmco ${⊢}\mathrm{dom}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)={{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}}^{-1}\left[\mathrm{dom}{F}\right]$
10 fndm ${⊢}{F}Fn\left({A}×{B}\right)\to \mathrm{dom}{F}={A}×{B}$
11 10 adantr ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to \mathrm{dom}{F}={A}×{B}$
12 11 imaeq2d ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to {{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}}^{-1}\left[\mathrm{dom}{F}\right]={{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}}^{-1}\left[{A}×{B}\right]$
13 imacnvcnv ${⊢}{{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}}^{-1}\left[{A}×{B}\right]=\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)\left[{A}×{B}\right]$
14 df-ima ${⊢}\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)\left[{A}×{B}\right]=\mathrm{ran}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)↾}_{\left({A}×{B}\right)}\right)$
15 resres ${⊢}{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)↾}_{\left({A}×{B}\right)}={{1}^{st}↾}_{\left(\left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)\right)}$
16 15 rneqi ${⊢}\mathrm{ran}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)↾}_{\left({A}×{B}\right)}\right)=\mathrm{ran}\left({{1}^{st}↾}_{\left(\left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)\right)}\right)$
17 13 14 16 3eqtri ${⊢}{{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}}^{-1}\left[{A}×{B}\right]=\mathrm{ran}\left({{1}^{st}↾}_{\left(\left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)\right)}\right)$
18 inxp ${⊢}\left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)=\left(\mathrm{V}\cap {A}\right)×\left(\left\{{C}\right\}\cap {B}\right)$
19 incom ${⊢}\mathrm{V}\cap {A}={A}\cap \mathrm{V}$
20 inv1 ${⊢}{A}\cap \mathrm{V}={A}$
21 19 20 eqtri ${⊢}\mathrm{V}\cap {A}={A}$
22 21 xpeq1i ${⊢}\left(\mathrm{V}\cap {A}\right)×\left(\left\{{C}\right\}\cap {B}\right)={A}×\left(\left\{{C}\right\}\cap {B}\right)$
23 18 22 eqtri ${⊢}\left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)={A}×\left(\left\{{C}\right\}\cap {B}\right)$
24 snssi ${⊢}{C}\in {B}\to \left\{{C}\right\}\subseteq {B}$
25 df-ss ${⊢}\left\{{C}\right\}\subseteq {B}↔\left\{{C}\right\}\cap {B}=\left\{{C}\right\}$
26 24 25 sylib ${⊢}{C}\in {B}\to \left\{{C}\right\}\cap {B}=\left\{{C}\right\}$
27 26 xpeq2d ${⊢}{C}\in {B}\to {A}×\left(\left\{{C}\right\}\cap {B}\right)={A}×\left\{{C}\right\}$
28 23 27 syl5eq ${⊢}{C}\in {B}\to \left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)={A}×\left\{{C}\right\}$
29 28 reseq2d ${⊢}{C}\in {B}\to {{1}^{st}↾}_{\left(\left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)\right)}={{1}^{st}↾}_{\left({A}×\left\{{C}\right\}\right)}$
30 29 rneqd ${⊢}{C}\in {B}\to \mathrm{ran}\left({{1}^{st}↾}_{\left(\left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)\right)}\right)=\mathrm{ran}\left({{1}^{st}↾}_{\left({A}×\left\{{C}\right\}\right)}\right)$
31 1stconst ${⊢}{C}\in {B}\to \left({{1}^{st}↾}_{\left({A}×\left\{{C}\right\}\right)}\right):{A}×\left\{{C}\right\}\underset{1-1 onto}{⟶}{A}$
32 f1ofo ${⊢}\left({{1}^{st}↾}_{\left({A}×\left\{{C}\right\}\right)}\right):{A}×\left\{{C}\right\}\underset{1-1 onto}{⟶}{A}\to \left({{1}^{st}↾}_{\left({A}×\left\{{C}\right\}\right)}\right):{A}×\left\{{C}\right\}\underset{onto}{⟶}{A}$
33 forn ${⊢}\left({{1}^{st}↾}_{\left({A}×\left\{{C}\right\}\right)}\right):{A}×\left\{{C}\right\}\underset{onto}{⟶}{A}\to \mathrm{ran}\left({{1}^{st}↾}_{\left({A}×\left\{{C}\right\}\right)}\right)={A}$
34 31 32 33 3syl ${⊢}{C}\in {B}\to \mathrm{ran}\left({{1}^{st}↾}_{\left({A}×\left\{{C}\right\}\right)}\right)={A}$
35 30 34 eqtrd ${⊢}{C}\in {B}\to \mathrm{ran}\left({{1}^{st}↾}_{\left(\left(\mathrm{V}×\left\{{C}\right\}\right)\cap \left({A}×{B}\right)\right)}\right)={A}$
36 17 35 syl5eq ${⊢}{C}\in {B}\to {{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}}^{-1}\left[{A}×{B}\right]={A}$
37 36 adantl ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to {{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}}^{-1}\left[{A}×{B}\right]={A}$
38 12 37 eqtrd ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to {{\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}}^{-1}\left[\mathrm{dom}{F}\right]={A}$
39 9 38 syl5eq ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to \mathrm{dom}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)={A}$
40 1 fneq1i ${⊢}{G}Fn{A}↔\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)Fn{A}$
41 df-fn ${⊢}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)Fn{A}↔\left(\mathrm{Fun}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)\wedge \mathrm{dom}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)={A}\right)$
42 40 41 bitri ${⊢}{G}Fn{A}↔\left(\mathrm{Fun}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)\wedge \mathrm{dom}\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)={A}\right)$
43 8 39 42 sylanbrc ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to {G}Fn{A}$
44 dffn5 ${⊢}{G}Fn{A}↔{G}=\left({x}\in {A}⟼{G}\left({x}\right)\right)$
45 43 44 sylib ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to {G}=\left({x}\in {A}⟼{G}\left({x}\right)\right)$
46 1 fveq1i ${⊢}{G}\left({x}\right)=\left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)\left({x}\right)$
47 dff1o4 ${⊢}\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right):\mathrm{V}×\left\{{C}\right\}\underset{1-1 onto}{⟶}\mathrm{V}↔\left(\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)Fn\left(\mathrm{V}×\left\{{C}\right\}\right)\wedge {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}Fn\mathrm{V}\right)$
48 3 47 sylib ${⊢}{C}\in {B}\to \left(\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)Fn\left(\mathrm{V}×\left\{{C}\right\}\right)\wedge {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}Fn\mathrm{V}\right)$
49 48 simprd ${⊢}{C}\in {B}\to {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}Fn\mathrm{V}$
50 vex ${⊢}{x}\in \mathrm{V}$
51 fvco2 ${⊢}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}Fn\mathrm{V}\wedge {x}\in \mathrm{V}\right)\to \left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)\left({x}\right)={F}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)\right)$
52 49 50 51 sylancl ${⊢}{C}\in {B}\to \left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)\left({x}\right)={F}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)\right)$
53 52 ad2antlr ${⊢}\left(\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\wedge {x}\in {A}\right)\to \left({F}\circ {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\right)\left({x}\right)={F}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)\right)$
54 46 53 syl5eq ${⊢}\left(\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\wedge {x}\in {A}\right)\to {G}\left({x}\right)={F}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)\right)$
55 3 adantr ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to \left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right):\mathrm{V}×\left\{{C}\right\}\underset{1-1 onto}{⟶}\mathrm{V}$
56 50 a1i ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to {x}\in \mathrm{V}$
57 snidg ${⊢}{C}\in {B}\to {C}\in \left\{{C}\right\}$
58 57 adantr ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to {C}\in \left\{{C}\right\}$
59 56 58 opelxpd ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to ⟨{x},{C}⟩\in \left(\mathrm{V}×\left\{{C}\right\}\right)$
60 55 59 jca ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to \left(\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right):\mathrm{V}×\left\{{C}\right\}\underset{1-1 onto}{⟶}\mathrm{V}\wedge ⟨{x},{C}⟩\in \left(\mathrm{V}×\left\{{C}\right\}\right)\right)$
61 50 a1i ${⊢}{C}\in {B}\to {x}\in \mathrm{V}$
62 61 57 opelxpd ${⊢}{C}\in {B}\to ⟨{x},{C}⟩\in \left(\mathrm{V}×\left\{{C}\right\}\right)$
63 62 fvresd ${⊢}{C}\in {B}\to \left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)\left(⟨{x},{C}⟩\right)={1}^{st}\left(⟨{x},{C}⟩\right)$
64 63 adantr ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to \left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)\left(⟨{x},{C}⟩\right)={1}^{st}\left(⟨{x},{C}⟩\right)$
65 op1stg ${⊢}\left({x}\in {A}\wedge {C}\in {B}\right)\to {1}^{st}\left(⟨{x},{C}⟩\right)={x}$
66 65 ancoms ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to {1}^{st}\left(⟨{x},{C}⟩\right)={x}$
67 64 66 eqtrd ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to \left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)\left(⟨{x},{C}⟩\right)={x}$
68 f1ocnvfv ${⊢}\left(\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right):\mathrm{V}×\left\{{C}\right\}\underset{1-1 onto}{⟶}\mathrm{V}\wedge ⟨{x},{C}⟩\in \left(\mathrm{V}×\left\{{C}\right\}\right)\right)\to \left(\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)\left(⟨{x},{C}⟩\right)={x}\to {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)=⟨{x},{C}⟩\right)$
69 60 67 68 sylc ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to {\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)=⟨{x},{C}⟩$
70 69 fveq2d ${⊢}\left({C}\in {B}\wedge {x}\in {A}\right)\to {F}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)\right)={F}\left(⟨{x},{C}⟩\right)$
71 70 adantll ${⊢}\left(\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\wedge {x}\in {A}\right)\to {F}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)\right)={F}\left(⟨{x},{C}⟩\right)$
72 df-ov ${⊢}{x}{F}{C}={F}\left(⟨{x},{C}⟩\right)$
73 71 72 syl6eqr ${⊢}\left(\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\wedge {x}\in {A}\right)\to {F}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\left\{{C}\right\}\right)}\right)}^{-1}\left({x}\right)\right)={x}{F}{C}$
74 54 73 eqtrd ${⊢}\left(\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\wedge {x}\in {A}\right)\to {G}\left({x}\right)={x}{F}{C}$
75 74 mpteq2dva ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to \left({x}\in {A}⟼{G}\left({x}\right)\right)=\left({x}\in {A}⟼{x}{F}{C}\right)$
76 45 75 eqtrd ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {C}\in {B}\right)\to {G}=\left({x}\in {A}⟼{x}{F}{C}\right)$