Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-cur | Structured version Visualization version GIF version |
Description: Define the currying of 𝐹, which splits a function of two arguments into a function of the first argument, producing a function over the second argument. (Contributed by Mario Carneiro, 7-Jan-2017.) |
Ref | Expression |
---|---|
df-cur | ⊢ curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cF | . . 3 class 𝐹 | |
2 | 1 | ccur 7973 | . 2 class curry 𝐹 |
3 | vx | . . 3 setvar 𝑥 | |
4 | 1 | cdm 5535 | . . . 4 class dom 𝐹 |
5 | 4 | cdm 5535 | . . 3 class dom dom 𝐹 |
6 | 3 | cv 1541 | . . . . . 6 class 𝑥 |
7 | vy | . . . . . . 7 setvar 𝑦 | |
8 | 7 | cv 1541 | . . . . . 6 class 𝑦 |
9 | 6, 8 | cop 4532 | . . . . 5 class 〈𝑥, 𝑦〉 |
10 | vz | . . . . . 6 setvar 𝑧 | |
11 | 10 | cv 1541 | . . . . 5 class 𝑧 |
12 | 9, 11, 1 | wbr 5040 | . . . 4 wff 〈𝑥, 𝑦〉𝐹𝑧 |
13 | 12, 7, 10 | copab 5102 | . . 3 class {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧} |
14 | 3, 5, 13 | cmpt 5120 | . 2 class (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) |
15 | 2, 14 | wceq 1542 | 1 wff curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {〈𝑦, 𝑧〉 ∣ 〈𝑥, 𝑦〉𝐹𝑧}) |
Colors of variables: wff setvar class |
This definition is referenced by: mpocurryd 7977 cureq 35409 curf 35411 curunc 35415 matunitlindf 35431 |
Copyright terms: Public domain | W3C validator |