Metamath Proof Explorer

Theorem curry1val

Description: The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Hypothesis	curry1.1	$⊢ G = F \circ {({2^{nd} ↾}_{(\{C\} \times V)})}^{-1}$
	Assertion	curry1val	$⊢ (F Fn (A \times B) \land C \in A) \to G (D) = C F D$

Proof

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