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 {({1^{st} ↾}_{(V \times \{C\})})}^{-1}$
	Assertion	curry2f	$⊢ (F : A \times B ⟶ D \land C \in B) \to G : A ⟶ D$

Step	Hyp	Ref	Expression
1		curry2.1	$⊢ G = F \circ {({1^{st} ↾}_{(V \times \{C\})})}^{-1}$
2		ffn	$⊢ F : A \times B ⟶ D \to F Fn (A \times B)$
3	1	curry2	$⊢ (F Fn (A \times B) \land C \in B) \to G = (x \in A ⟼ x F C)$
4	2 3	sylan	$⊢ (F : A \times B ⟶ D \land C \in B) \to G = (x \in A ⟼ x F C)$
5		fovcdm	$⊢ (F : A \times B ⟶ D \land x \in A \land C \in B) \to x F C \in D$
6	5	3com23	$⊢ (F : A \times B ⟶ D \land C \in B \land x \in A) \to x F C \in D$
7	6	3expa	$⊢ ((F : A \times B ⟶ D \land C \in B) \land x \in A) \to x F C \in D$
8	4 7	fmpt3d	$⊢ (F : A \times B ⟶ D \land C \in B) \to G : A ⟶ D$

Metamath Proof Explorer