Theorem curry1f

Description: Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008)

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

Proof

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