Metamath Proof Explorer


Theorem unccur

Description: Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021)

Ref Expression
Assertion unccur F : A × B C B V C W uncurry curry F = F

Proof

Step Hyp Ref Expression
1 ffn F : A × B C F Fn A × B
2 1 anim1i F : A × B C B V F Fn A × B B V
3 2 3adant3 F : A × B C B V C W F Fn A × B B V
4 3anass F Fn A × B x A y B F Fn A × B x A y B
5 curfv F Fn A × B x A y B B V curry F x y = x F y
6 4 5 sylanbr F Fn A × B x A y B B V curry F x y = x F y
7 6 an32s F Fn A × B B V x A y B curry F x y = x F y
8 7 eqeq1d F Fn A × B B V x A y B curry F x y = z x F y = z
9 eqcom x F y = z z = x F y
10 8 9 bitrdi F Fn A × B B V x A y B curry F x y = z z = x F y
11 3 10 sylan F : A × B C B V C W x A y B curry F x y = z z = x F y
12 curf F : A × B C B V C W curry F : A C B
13 12 ffvelrnda F : A × B C B V C W x A curry F x C B
14 elmapfn curry F x C B curry F x Fn B
15 13 14 syl F : A × B C B V C W x A curry F x Fn B
16 fnbrfvb curry F x Fn B y B curry F x y = z y curry F x z
17 15 16 sylan F : A × B C B V C W x A y B curry F x y = z y curry F x z
18 17 anasss F : A × B C B V C W x A y B curry F x y = z y curry F x z
19 ibar x A y B z = x F y x A y B z = x F y
20 19 adantl F : A × B C B V C W x A y B z = x F y x A y B z = x F y
21 11 18 20 3bitr3d F : A × B C B V C W x A y B y curry F x z x A y B z = x F y
22 df-br y curry F x z y z curry F x
23 elfvdm y z curry F x x dom curry F
24 22 23 sylbi y curry F x z x dom curry F
25 fdm curry F : A C B dom curry F = A
26 25 eleq2d curry F : A C B x dom curry F x A
27 26 biimpa curry F : A C B x dom curry F x A
28 24 27 sylan2 curry F : A C B y curry F x z x A
29 ffvelrn curry F : A C B x A curry F x C B
30 elmapi curry F x C B curry F x : B C
31 fdm curry F x : B C dom curry F x = B
32 29 30 31 3syl curry F : A C B x A dom curry F x = B
33 vex y V
34 vex z V
35 33 34 breldm y curry F x z y dom curry F x
36 eleq2 dom curry F x = B y dom curry F x y B
37 36 biimpa dom curry F x = B y dom curry F x y B
38 32 35 37 syl2an curry F : A C B x A y curry F x z y B
39 38 an32s curry F : A C B y curry F x z x A y B
40 28 39 mpdan curry F : A C B y curry F x z y B
41 28 40 jca curry F : A C B y curry F x z x A y B
42 12 41 sylan F : A × B C B V C W y curry F x z x A y B
43 42 stoic1a F : A × B C B V C W ¬ x A y B ¬ y curry F x z
44 simpl x A y B z = x F y x A y B
45 44 con3i ¬ x A y B ¬ x A y B z = x F y
46 45 adantl F : A × B C B V C W ¬ x A y B ¬ x A y B z = x F y
47 43 46 2falsed F : A × B C B V C W ¬ x A y B y curry F x z x A y B z = x F y
48 21 47 pm2.61dan F : A × B C B V C W y curry F x z x A y B z = x F y
49 48 oprabbidv F : A × B C B V C W x y z | y curry F x z = x y z | x A y B z = x F y
50 df-unc uncurry curry F = x y z | y curry F x z
51 df-mpo x A , y B x F y = x y z | x A y B z = x F y
52 49 50 51 3eqtr4g F : A × B C B V C W uncurry curry F = x A , y B x F y
53 fnov F Fn A × B F = x A , y B x F y
54 1 53 sylib F : A × B C F = x A , y B x F y
55 54 3ad2ant1 F : A × B C B V C W F = x A , y B x F y
56 52 55 eqtr4d F : A × B C B V C W uncurry curry F = F