Description: Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | uncf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffvelrn | |
|
2 | elmapi | |
|
3 | 1 2 | syl | |
4 | 3 | ffvelrnda | |
5 | 4 | anasss | |
6 | 5 | ralrimivva | |
7 | df-unc | |
|
8 | df-br | |
|
9 | elfvdm | |
|
10 | 8 9 | sylbi | |
11 | fdm | |
|
12 | 11 | eleq2d | |
13 | 10 12 | syl5ib | |
14 | 13 | pm4.71rd | |
15 | elmapfun | |
|
16 | funbrfv2b | |
|
17 | 1 15 16 | 3syl | |
18 | fdm | |
|
19 | 1 2 18 | 3syl | |
20 | 19 | eleq2d | |
21 | eqcom | |
|
22 | 21 | a1i | |
23 | 20 22 | anbi12d | |
24 | 17 23 | bitrd | |
25 | 24 | pm5.32da | |
26 | 14 25 | bitrd | |
27 | anass | |
|
28 | 26 27 | bitr4di | |
29 | 28 | oprabbidv | |
30 | 7 29 | eqtrid | |
31 | 30 | feq1d | |
32 | df-mpo | |
|
33 | 32 | eqcomi | |
34 | 33 | fmpo | |
35 | 31 34 | bitr4di | |
36 | 6 35 | mpbird | |