Theorem curry2f

Description: Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008)

	Ref	Expression
Hypothesis	curry2.1	$$⊢G=F\circ {\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \left\{C\right\}\right)}\right)}^{-1}$$
Assertion	curry2f	$$⊢\left(F:A\times B⟶D\wedge C\in B\right)\to G:A⟶D$$

Proof

Step	Hyp	Ref	Expression
1		curry2.1	$$⊢G=F\circ {\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \left\{C\right\}\right)}\right)}^{-1}$$
2		ffn	$$⊢F:A\times B⟶D\to FFn\left(A\times B\right)$$
3	1	curry2	$$⊢\left(FFn\left(A\times B\right)\wedge C\in B\right)\to G=\left(x\in A⟼xFC\right)$$
4	2 3	sylan	$$⊢\left(F:A\times B⟶D\wedge C\in B\right)\to G=\left(x\in A⟼xFC\right)$$
5		fovrn	$$⊢\left(F:A\times B⟶D\wedge x\in A\wedge C\in B\right)\to xFC\in D$$
6	5	3com23	$$⊢\left(F:A\times B⟶D\wedge C\in B\wedge x\in A\right)\to xFC\in D$$
7	6	3expa	$$⊢\left(\left(F:A\times B⟶D\wedge C\in B\right)\wedge x\in A\right)\to xFC\in D$$
8	4 7	fmpt3d	$$⊢\left(F:A\times B⟶D\wedge C\in B\right)\to G:A⟶D$$