Metamath Proof Explorer


Theorem uncf

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

Ref Expression
Assertion uncf F:ACBuncurryF:A×BC

Proof

Step Hyp Ref Expression
1 ffvelrn F:ACBxAFxCB
2 elmapi FxCBFx:BC
3 1 2 syl F:ACBxAFx:BC
4 3 ffvelrnda F:ACBxAyBFxyC
5 4 anasss F:ACBxAyBFxyC
6 5 ralrimivva F:ACBxAyBFxyC
7 df-unc uncurryF=xyz|yFxz
8 df-br yFxzyzFx
9 elfvdm yzFxxdomF
10 8 9 sylbi yFxzxdomF
11 fdm F:ACBdomF=A
12 11 eleq2d F:ACBxdomFxA
13 10 12 syl5ib F:ACByFxzxA
14 13 pm4.71rd F:ACByFxzxAyFxz
15 elmapfun FxCBFunFx
16 funbrfv2b FunFxyFxzydomFxFxy=z
17 1 15 16 3syl F:ACBxAyFxzydomFxFxy=z
18 fdm Fx:BCdomFx=B
19 1 2 18 3syl F:ACBxAdomFx=B
20 19 eleq2d F:ACBxAydomFxyB
21 eqcom Fxy=zz=Fxy
22 21 a1i F:ACBxAFxy=zz=Fxy
23 20 22 anbi12d F:ACBxAydomFxFxy=zyBz=Fxy
24 17 23 bitrd F:ACBxAyFxzyBz=Fxy
25 24 pm5.32da F:ACBxAyFxzxAyBz=Fxy
26 14 25 bitrd F:ACByFxzxAyBz=Fxy
27 anass xAyBz=FxyxAyBz=Fxy
28 26 27 bitr4di F:ACByFxzxAyBz=Fxy
29 28 oprabbidv F:ACBxyz|yFxz=xyz|xAyBz=Fxy
30 7 29 eqtrid F:ACBuncurryF=xyz|xAyBz=Fxy
31 30 feq1d F:ACBuncurryF:A×BCxyz|xAyBz=Fxy:A×BC
32 df-mpo xA,yBFxy=xyz|xAyBz=Fxy
33 32 eqcomi xyz|xAyBz=Fxy=xA,yBFxy
34 33 fmpo xAyBFxyCxyz|xAyBz=Fxy:A×BC
35 31 34 bitr4di F:ACBuncurryF:A×BCxAyBFxyC
36 6 35 mpbird F:ACBuncurryF:A×BC