Metamath Proof Explorer


Theorem curfv

Description: Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion curfv F Fn V × W A V B W W X curry F A B = A F B

Proof

Step Hyp Ref Expression
1 dffn5 F Fn V × W F = z V × W F z
2 cureq F = z V × W F z curry F = curry z V × W F z
3 1 2 sylbi F Fn V × W curry F = curry z V × W F z
4 3 adantr F Fn V × W B W curry F = curry z V × W F z
5 fveq2 z = x y F z = F x y
6 5 mpompt z V × W F z = x V , y W F x y
7 fvex F x y V
8 7 rgen2w x V y W F x y V
9 8 a1i F Fn V × W B W x V y W F x y V
10 ne0i B W W
11 10 adantl F Fn V × W B W W
12 6 9 11 mpocurryd F Fn V × W B W curry z V × W F z = x V y W F x y
13 4 12 eqtrd F Fn V × W B W curry F = x V y W F x y
14 13 3adant2 F Fn V × W A V B W curry F = x V y W F x y
15 14 fveq1d F Fn V × W A V B W curry F A = x V y W F x y A
16 15 adantr F Fn V × W A V B W W X curry F A = x V y W F x y A
17 mptexg W X y W F A y V
18 opeq1 x = A x y = A y
19 18 fveq2d x = A F x y = F A y
20 19 mpteq2dv x = A y W F x y = y W F A y
21 eqid x V y W F x y = x V y W F x y
22 20 21 fvmptg A V y W F A y V x V y W F x y A = y W F A y
23 17 22 sylan2 A V W X x V y W F x y A = y W F A y
24 23 3ad2antl2 F Fn V × W A V B W W X x V y W F x y A = y W F A y
25 16 24 eqtrd F Fn V × W A V B W W X curry F A = y W F A y
26 25 fveq1d F Fn V × W A V B W W X curry F A B = y W F A y B
27 opeq2 y = B A y = A B
28 27 fveq2d y = B F A y = F A B
29 eqid y W F A y = y W F A y
30 fvex F A B V
31 28 29 30 fvmpt B W y W F A y B = F A B
32 df-ov A F B = F A B
33 31 32 eqtr4di B W y W F A y B = A F B
34 33 3ad2ant3 F Fn V × W A V B W y W F A y B = A F B
35 34 adantr F Fn V × W A V B W W X y W F A y B = A F B
36 26 35 eqtrd F Fn V × W A V B W W X curry F A B = A F B