# Metamath Proof Explorer

## Theorem curfv

Description: Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion curfv ${⊢}\left(\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\wedge {W}\in {X}\right)\to curry{F}\left({A}\right)\left({B}\right)={A}{F}{B}$

### Proof

Step Hyp Ref Expression
1 dffn5 ${⊢}{F}Fn\left({V}×{W}\right)↔{F}=\left({z}\in \left({V}×{W}\right)⟼{F}\left({z}\right)\right)$
2 cureq ${⊢}{F}=\left({z}\in \left({V}×{W}\right)⟼{F}\left({z}\right)\right)\to curry{F}=curry\left({z}\in \left({V}×{W}\right)⟼{F}\left({z}\right)\right)$
3 1 2 sylbi ${⊢}{F}Fn\left({V}×{W}\right)\to curry{F}=curry\left({z}\in \left({V}×{W}\right)⟼{F}\left({z}\right)\right)$
4 3 adantr ${⊢}\left({F}Fn\left({V}×{W}\right)\wedge {B}\in {W}\right)\to curry{F}=curry\left({z}\in \left({V}×{W}\right)⟼{F}\left({z}\right)\right)$
5 fveq2 ${⊢}{z}=⟨{x},{y}⟩\to {F}\left({z}\right)={F}\left(⟨{x},{y}⟩\right)$
6 5 mpompt ${⊢}\left({z}\in \left({V}×{W}\right)⟼{F}\left({z}\right)\right)=\left({x}\in {V},{y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)$
7 fvex ${⊢}{F}\left(⟨{x},{y}⟩\right)\in \mathrm{V}$
8 7 rgen2w ${⊢}\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {W}\phantom{\rule{.4em}{0ex}}{F}\left(⟨{x},{y}⟩\right)\in \mathrm{V}$
9 8 a1i ${⊢}\left({F}Fn\left({V}×{W}\right)\wedge {B}\in {W}\right)\to \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {W}\phantom{\rule{.4em}{0ex}}{F}\left(⟨{x},{y}⟩\right)\in \mathrm{V}$
10 ne0i ${⊢}{B}\in {W}\to {W}\ne \varnothing$
11 10 adantl ${⊢}\left({F}Fn\left({V}×{W}\right)\wedge {B}\in {W}\right)\to {W}\ne \varnothing$
12 6 9 11 mpocurryd ${⊢}\left({F}Fn\left({V}×{W}\right)\wedge {B}\in {W}\right)\to curry\left({z}\in \left({V}×{W}\right)⟼{F}\left({z}\right)\right)=\left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)$
13 4 12 eqtrd ${⊢}\left({F}Fn\left({V}×{W}\right)\wedge {B}\in {W}\right)\to curry{F}=\left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)$
14 13 3adant2 ${⊢}\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\to curry{F}=\left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)$
15 14 fveq1d ${⊢}\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\to curry{F}\left({A}\right)=\left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)\left({A}\right)$
16 15 adantr ${⊢}\left(\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\wedge {W}\in {X}\right)\to curry{F}\left({A}\right)=\left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)\left({A}\right)$
17 mptexg ${⊢}{W}\in {X}\to \left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)\in \mathrm{V}$
18 opeq1 ${⊢}{x}={A}\to ⟨{x},{y}⟩=⟨{A},{y}⟩$
19 18 fveq2d ${⊢}{x}={A}\to {F}\left(⟨{x},{y}⟩\right)={F}\left(⟨{A},{y}⟩\right)$
20 19 mpteq2dv ${⊢}{x}={A}\to \left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)=\left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)$
21 eqid ${⊢}\left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)=\left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)$
22 20 21 fvmptg ${⊢}\left({A}\in {V}\wedge \left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)\in \mathrm{V}\right)\to \left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)\left({A}\right)=\left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)$
23 17 22 sylan2 ${⊢}\left({A}\in {V}\wedge {W}\in {X}\right)\to \left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)\left({A}\right)=\left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)$
24 23 3ad2antl2 ${⊢}\left(\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\wedge {W}\in {X}\right)\to \left({x}\in {V}⟼\left({y}\in {W}⟼{F}\left(⟨{x},{y}⟩\right)\right)\right)\left({A}\right)=\left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)$
25 16 24 eqtrd ${⊢}\left(\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\wedge {W}\in {X}\right)\to curry{F}\left({A}\right)=\left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)$
26 25 fveq1d ${⊢}\left(\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\wedge {W}\in {X}\right)\to curry{F}\left({A}\right)\left({B}\right)=\left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)\left({B}\right)$
27 opeq2 ${⊢}{y}={B}\to ⟨{A},{y}⟩=⟨{A},{B}⟩$
28 27 fveq2d ${⊢}{y}={B}\to {F}\left(⟨{A},{y}⟩\right)={F}\left(⟨{A},{B}⟩\right)$
29 eqid ${⊢}\left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)=\left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)$
30 fvex ${⊢}{F}\left(⟨{A},{B}⟩\right)\in \mathrm{V}$
31 28 29 30 fvmpt ${⊢}{B}\in {W}\to \left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)\left({B}\right)={F}\left(⟨{A},{B}⟩\right)$
32 df-ov ${⊢}{A}{F}{B}={F}\left(⟨{A},{B}⟩\right)$
33 31 32 syl6eqr ${⊢}{B}\in {W}\to \left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)\left({B}\right)={A}{F}{B}$
34 33 3ad2ant3 ${⊢}\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\to \left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)\left({B}\right)={A}{F}{B}$
35 34 adantr ${⊢}\left(\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\wedge {W}\in {X}\right)\to \left({y}\in {W}⟼{F}\left(⟨{A},{y}⟩\right)\right)\left({B}\right)={A}{F}{B}$
36 26 35 eqtrd ${⊢}\left(\left({F}Fn\left({V}×{W}\right)\wedge {A}\in {V}\wedge {B}\in {W}\right)\wedge {W}\in {X}\right)\to curry{F}\left({A}\right)\left({B}\right)={A}{F}{B}$