curfv

		Ref	Expression
	Assertion	curfv	$⊢ ((F Fn (V \times W) \land A \in V \land B \in W) \land W \in X) \to curry F (A) (B) = A F B$

Proof

Step	Hyp	Ref	Expression
1		dffn5	$⊢ F Fn (V \times W) \leftrightarrow F = (z \in (V \times W) ⟼ F (z))$
2		cureq	$⊢ F = (z \in (V \times W) ⟼ F (z)) \to curry F = curry (z \in (V \times W) ⟼ F (z))$
3	1 2	sylbi	$⊢ F Fn (V \times W) \to curry F = curry (z \in (V \times W) ⟼ F (z))$
4	3	adantr	$⊢ (F Fn (V \times W) \land B \in W) \to curry F = curry (z \in (V \times W) ⟼ F (z))$
5		fveq2	$⊢ z = ⟨x, y⟩ \to F (z) = F (⟨x, y⟩)$
6	5	mpompt	$⊢ (z \in (V \times W) ⟼ F (z)) = (x \in V, y \in W ⟼ F (⟨x, y⟩))$
7		fvex	$⊢ F (⟨x, y⟩) \in V$
8	7	rgen2w	$⊢ \forall x \in V \forall y \in W F (⟨x, y⟩) \in V$
9	8	a1i	$⊢ (F Fn (V \times W) \land B \in W) \to \forall x \in V \forall y \in W F (⟨x, y⟩) \in V$
10		ne0i	$⊢ B \in W \to W \neq \emptyset$
11	10	adantl	$⊢ (F Fn (V \times W) \land B \in W) \to W \neq \emptyset$
12	6 9 11	mpocurryd	$⊢ (F Fn (V \times W) \land B \in W) \to curry (z \in (V \times W) ⟼ F (z)) = (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩)))$
13	4 12	eqtrd	$⊢ (F Fn (V \times W) \land B \in W) \to curry F = (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩)))$
14	13	3adant2	$⊢ (F Fn (V \times W) \land A \in V \land B \in W) \to curry F = (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩)))$
15	14	fveq1d	$⊢ (F Fn (V \times W) \land A \in V \land B \in W) \to curry F (A) = (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩))) (A)$
16	15	adantr	$⊢ ((F Fn (V \times W) \land A \in V \land B \in W) \land W \in X) \to curry F (A) = (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩))) (A)$
17		mptexg	$⊢ W \in X \to (y \in W ⟼ F (⟨A, y⟩)) \in V$
18		opeq1	$⊢ x = A \to ⟨x, y⟩ = ⟨A, y⟩$
19	18	fveq2d	$⊢ x = A \to F (⟨x, y⟩) = F (⟨A, y⟩)$
20	19	mpteq2dv	$⊢ x = A \to (y \in W ⟼ F (⟨x, y⟩)) = (y \in W ⟼ F (⟨A, y⟩))$
21		eqid	$⊢ (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩))) = (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩)))$
22	20 21	fvmptg	$⊢ (A \in V \land (y \in W ⟼ F (⟨A, y⟩)) \in V) \to (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩))) (A) = (y \in W ⟼ F (⟨A, y⟩))$
23	17 22	sylan2	$⊢ (A \in V \land W \in X) \to (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩))) (A) = (y \in W ⟼ F (⟨A, y⟩))$
24	23	3ad2antl2	$⊢ ((F Fn (V \times W) \land A \in V \land B \in W) \land W \in X) \to (x \in V ⟼ (y \in W ⟼ F (⟨x, y⟩))) (A) = (y \in W ⟼ F (⟨A, y⟩))$
25	16 24	eqtrd	$⊢ ((F Fn (V \times W) \land A \in V \land B \in W) \land W \in X) \to curry F (A) = (y \in W ⟼ F (⟨A, y⟩))$
26	25	fveq1d	$⊢ ((F Fn (V \times W) \land A \in V \land B \in W) \land W \in X) \to curry F (A) (B) = (y \in W ⟼ F (⟨A, y⟩)) (B)$
27		opeq2	$⊢ y = B \to ⟨A, y⟩ = ⟨A, B⟩$
28	27	fveq2d	$⊢ y = B \to F (⟨A, y⟩) = F (⟨A, B⟩)$
29		eqid	$⊢ (y \in W ⟼ F (⟨A, y⟩)) = (y \in W ⟼ F (⟨A, y⟩))$
30		fvex	$⊢ F (⟨A, B⟩) \in V$
31	28 29 30	fvmpt	$⊢ B \in W \to (y \in W ⟼ F (⟨A, y⟩)) (B) = F (⟨A, B⟩)$
32		df-ov	$⊢ A F B = F (⟨A, B⟩)$
33	31 32	eqtr4di	$⊢ B \in W \to (y \in W ⟼ F (⟨A, y⟩)) (B) = A F B$
34	33	3ad2ant3	$⊢ (F Fn (V \times W) \land A \in V \land B \in W) \to (y \in W ⟼ F (⟨A, y⟩)) (B) = A F B$
35	34	adantr	$⊢ ((F Fn (V \times W) \land A \in V \land B \in W) \land W \in X) \to (y \in W ⟼ F (⟨A, y⟩)) (B) = A F B$
36	26 35	eqtrd	$⊢ ((F Fn (V \times W) \land A \in V \land B \in W) \land W \in X) \to curry F (A) (B) = A F B$

Metamath Proof Explorer

Theorem curfv

Proof