# Metamath Proof Explorer

## Theorem curunc

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

Ref Expression
Assertion curunc ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\to curryuncurry{F}={F}$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\to {F}:{A}⟶{{C}}^{{B}}$
2 1 feqmptd ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\to {F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
3 uncf ${⊢}{F}:{A}⟶{{C}}^{{B}}\to uncurry{F}:{A}×{B}⟶{C}$
4 3 fdmd ${⊢}{F}:{A}⟶{{C}}^{{B}}\to \mathrm{dom}uncurry{F}={A}×{B}$
5 4 dmeqd ${⊢}{F}:{A}⟶{{C}}^{{B}}\to \mathrm{dom}\mathrm{dom}uncurry{F}=\mathrm{dom}\left({A}×{B}\right)$
6 dmxp ${⊢}{B}\ne \varnothing \to \mathrm{dom}\left({A}×{B}\right)={A}$
7 5 6 sylan9eq ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\to \mathrm{dom}\mathrm{dom}uncurry{F}={A}$
8 7 eqcomd ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\to {A}=\mathrm{dom}\mathrm{dom}uncurry{F}$
9 df-mpt ${⊢}\left({y}\in {B}⟼{F}\left({x}\right)\left({y}\right)\right)=\left\{⟨{y},{z}⟩|\left({y}\in {B}\wedge {z}={F}\left({x}\right)\left({y}\right)\right)\right\}$
10 ffvelrn ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in \left({{C}}^{{B}}\right)$
11 elmapi ${⊢}{F}\left({x}\right)\in \left({{C}}^{{B}}\right)\to {F}\left({x}\right):{B}⟶{C}$
12 10 11 syl ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to {F}\left({x}\right):{B}⟶{C}$
13 12 feqmptd ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to {F}\left({x}\right)=\left({y}\in {B}⟼{F}\left({x}\right)\left({y}\right)\right)$
14 ffun ${⊢}uncurry{F}:{A}×{B}⟶{C}\to \mathrm{Fun}uncurry{F}$
15 funbrfv2b ${⊢}\mathrm{Fun}uncurry{F}\to \left(⟨{x},{y}⟩uncurry{F}{z}↔\left(⟨{x},{y}⟩\in \mathrm{dom}uncurry{F}\wedge uncurry{F}\left(⟨{x},{y}⟩\right)={z}\right)\right)$
16 3 14 15 3syl ${⊢}{F}:{A}⟶{{C}}^{{B}}\to \left(⟨{x},{y}⟩uncurry{F}{z}↔\left(⟨{x},{y}⟩\in \mathrm{dom}uncurry{F}\wedge uncurry{F}\left(⟨{x},{y}⟩\right)={z}\right)\right)$
17 16 adantr ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to \left(⟨{x},{y}⟩uncurry{F}{z}↔\left(⟨{x},{y}⟩\in \mathrm{dom}uncurry{F}\wedge uncurry{F}\left(⟨{x},{y}⟩\right)={z}\right)\right)$
18 4 eleq2d ${⊢}{F}:{A}⟶{{C}}^{{B}}\to \left(⟨{x},{y}⟩\in \mathrm{dom}uncurry{F}↔⟨{x},{y}⟩\in \left({A}×{B}\right)\right)$
19 opelxp ${⊢}⟨{x},{y}⟩\in \left({A}×{B}\right)↔\left({x}\in {A}\wedge {y}\in {B}\right)$
20 19 baib ${⊢}{x}\in {A}\to \left(⟨{x},{y}⟩\in \left({A}×{B}\right)↔{y}\in {B}\right)$
21 18 20 sylan9bb ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to \left(⟨{x},{y}⟩\in \mathrm{dom}uncurry{F}↔{y}\in {B}\right)$
22 df-ov ${⊢}{x}uncurry{F}{y}=uncurry{F}\left(⟨{x},{y}⟩\right)$
23 uncov ${⊢}\left({x}\in \mathrm{V}\wedge {y}\in \mathrm{V}\right)\to {x}uncurry{F}{y}={F}\left({x}\right)\left({y}\right)$
24 23 el2v ${⊢}{x}uncurry{F}{y}={F}\left({x}\right)\left({y}\right)$
25 22 24 eqtr3i ${⊢}uncurry{F}\left(⟨{x},{y}⟩\right)={F}\left({x}\right)\left({y}\right)$
26 25 eqeq1i ${⊢}uncurry{F}\left(⟨{x},{y}⟩\right)={z}↔{F}\left({x}\right)\left({y}\right)={z}$
27 eqcom ${⊢}{F}\left({x}\right)\left({y}\right)={z}↔{z}={F}\left({x}\right)\left({y}\right)$
28 26 27 bitri ${⊢}uncurry{F}\left(⟨{x},{y}⟩\right)={z}↔{z}={F}\left({x}\right)\left({y}\right)$
29 28 a1i ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to \left(uncurry{F}\left(⟨{x},{y}⟩\right)={z}↔{z}={F}\left({x}\right)\left({y}\right)\right)$
30 21 29 anbi12d ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to \left(\left(⟨{x},{y}⟩\in \mathrm{dom}uncurry{F}\wedge uncurry{F}\left(⟨{x},{y}⟩\right)={z}\right)↔\left({y}\in {B}\wedge {z}={F}\left({x}\right)\left({y}\right)\right)\right)$
31 17 30 bitrd ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to \left(⟨{x},{y}⟩uncurry{F}{z}↔\left({y}\in {B}\wedge {z}={F}\left({x}\right)\left({y}\right)\right)\right)$
32 31 opabbidv ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to \left\{⟨{y},{z}⟩|⟨{x},{y}⟩uncurry{F}{z}\right\}=\left\{⟨{y},{z}⟩|\left({y}\in {B}\wedge {z}={F}\left({x}\right)\left({y}\right)\right)\right\}$
33 9 13 32 3eqtr4a ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {x}\in {A}\right)\to {F}\left({x}\right)=\left\{⟨{y},{z}⟩|⟨{x},{y}⟩uncurry{F}{z}\right\}$
34 33 adantlr ${⊢}\left(\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\wedge {x}\in {A}\right)\to {F}\left({x}\right)=\left\{⟨{y},{z}⟩|⟨{x},{y}⟩uncurry{F}{z}\right\}$
35 8 34 mpteq12dva ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\to \left({x}\in {A}⟼{F}\left({x}\right)\right)=\left({x}\in \mathrm{dom}\mathrm{dom}uncurry{F}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩uncurry{F}{z}\right\}\right)$
36 df-cur ${⊢}curryuncurry{F}=\left({x}\in \mathrm{dom}\mathrm{dom}uncurry{F}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩uncurry{F}{z}\right\}\right)$
37 35 36 syl6eqr ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\to \left({x}\in {A}⟼{F}\left({x}\right)\right)=curryuncurry{F}$
38 2 37 eqtr2d ${⊢}\left({F}:{A}⟶{{C}}^{{B}}\wedge {B}\ne \varnothing \right)\to curryuncurry{F}={F}$