curry2val

Description: The value 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	curry2val	$⊢ (F Fn (A \times B) \land C \in B) \to G (D) = D F C$

Step	Hyp	Ref	Expression
1		curry2.1	$⊢ G = F \circ {({1^{st} ↾}_{(V \times \{C\})})}^{-1}$
2	1	curry2	$⊢ (F Fn (A \times B) \land C \in B) \to G = (x \in A ⟼ x F C)$
3	2	fveq1d	$⊢ (F Fn (A \times B) \land C \in B) \to G (D) = (x \in A ⟼ x F C) (D)$
4		eqid	$⊢ (x \in A ⟼ x F C) = (x \in A ⟼ x F C)$
5	4	fvmptndm	$⊢ \neg D \in A \to (x \in A ⟼ x F C) (D) = \emptyset$
6	5	adantl	$⊢ (F Fn (A \times B) \land \neg D \in A) \to (x \in A ⟼ x F C) (D) = \emptyset$
7		fndm	$⊢ F Fn (A \times B) \to dom F = A \times B$
8		simpl	$⊢ (D \in A \land C \in B) \to D \in A$
9	8	con3i	$⊢ \neg D \in A \to \neg (D \in A \land C \in B)$
10		ndmovg	$⊢ (dom F = A \times B \land \neg (D \in A \land C \in B)) \to D F C = \emptyset$
11	7 9 10	syl2an	$⊢ (F Fn (A \times B) \land \neg D \in A) \to D F C = \emptyset$
12	6 11	eqtr4d	$⊢ (F Fn (A \times B) \land \neg D \in A) \to (x \in A ⟼ x F C) (D) = D F C$
13	12	ex	$⊢ F Fn (A \times B) \to (\neg D \in A \to (x \in A ⟼ x F C) (D) = D F C)$
14	13	adantr	$⊢ (F Fn (A \times B) \land C \in B) \to (\neg D \in A \to (x \in A ⟼ x F C) (D) = D F C)$
15		oveq1	$⊢ x = D \to x F C = D F C$
16		ovex	$⊢ D F C \in V$
17	15 4 16	fvmpt	$⊢ D \in A \to (x \in A ⟼ x F C) (D) = D F C$
18	14 17	pm2.61d2	$⊢ (F Fn (A \times B) \land C \in B) \to (x \in A ⟼ x F C) (D) = D F C$
19	3 18	eqtrd	$⊢ (F Fn (A \times B) \land C \in B) \to G (D) = D F C$

Metamath Proof Explorer