Metamath Proof Explorer


Theorem curunc

Description: Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion curunc F : A C B B curry uncurry F = F

Proof

Step Hyp Ref Expression
1 simpl F : A C B B F : A C B
2 1 feqmptd F : A C B B F = x A F x
3 uncf F : A C B uncurry F : A × B C
4 3 fdmd F : A C B dom uncurry F = A × B
5 4 dmeqd F : A C B dom dom uncurry F = dom A × B
6 dmxp B dom A × B = A
7 5 6 sylan9eq F : A C B B dom dom uncurry F = A
8 7 eqcomd F : A C B B A = dom dom uncurry F
9 df-mpt y B F x y = y z | y B z = F x y
10 ffvelrn F : A C B x A F x C B
11 elmapi F x C B F x : B C
12 10 11 syl F : A C B x A F x : B C
13 12 feqmptd F : A C B x A F x = y B F x y
14 ffun uncurry F : A × B C Fun uncurry F
15 funbrfv2b Fun uncurry F x y uncurry F z x y dom uncurry F uncurry F x y = z
16 3 14 15 3syl F : A C B x y uncurry F z x y dom uncurry F uncurry F x y = z
17 16 adantr F : A C B x A x y uncurry F z x y dom uncurry F uncurry F x y = z
18 4 eleq2d F : A C B x y dom uncurry F x y A × B
19 opelxp x y A × B x A y B
20 19 baib x A x y A × B y B
21 18 20 sylan9bb F : A C B x A x y dom uncurry F y B
22 df-ov x uncurry F y = uncurry F x y
23 uncov x V y V x uncurry F y = F x y
24 23 el2v x uncurry F y = F x y
25 22 24 eqtr3i uncurry F x y = F x y
26 25 eqeq1i uncurry F x y = z F x y = z
27 eqcom F x y = z z = F x y
28 26 27 bitri uncurry F x y = z z = F x y
29 28 a1i F : A C B x A uncurry F x y = z z = F x y
30 21 29 anbi12d F : A C B x A x y dom uncurry F uncurry F x y = z y B z = F x y
31 17 30 bitrd F : A C B x A x y uncurry F z y B z = F x y
32 31 opabbidv F : A C B x A y z | x y uncurry F z = y z | y B z = F x y
33 9 13 32 3eqtr4a F : A C B x A F x = y z | x y uncurry F z
34 33 adantlr F : A C B B x A F x = y z | x y uncurry F z
35 8 34 mpteq12dva F : A C B B x A F x = x dom dom uncurry F y z | x y uncurry F z
36 df-cur curry uncurry F = x dom dom uncurry F y z | x y uncurry F z
37 35 36 syl6eqr F : A C B B x A F x = curry uncurry F
38 2 37 eqtr2d F : A C B B curry uncurry F = F