uncov

Description: Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021)

		Ref	Expression
	Assertion	uncov	$⊢ (A \in V \land B \in W) \to A uncurry F B = F (A) (B)$

Step	Hyp	Ref	Expression
1		df-br	$⊢ ⟨A, B⟩ uncurry F w \leftrightarrow ⟨⟨A, B⟩, w⟩ \in uncurry F$
2		df-unc	$⊢ uncurry F = \{⟨⟨x, y⟩, z⟩ \| y F (x) z\}$
3	2	eleq2i	$⊢ ⟨⟨A, B⟩, w⟩ \in uncurry F \leftrightarrow ⟨⟨A, B⟩, w⟩ \in \{⟨⟨x, y⟩, z⟩ \| y F (x) z\}$
4	1 3	bitri	$⊢ ⟨A, B⟩ uncurry F w \leftrightarrow ⟨⟨A, B⟩, w⟩ \in \{⟨⟨x, y⟩, z⟩ \| y F (x) z\}$
5		vex	$⊢ w \in V$
6		simp2	$⊢ (x = A \land y = B \land z = w) \to y = B$
7		fveq2	$⊢ x = A \to F (x) = F (A)$
8	7	3ad2ant1	$⊢ (x = A \land y = B \land z = w) \to F (x) = F (A)$
9		simp3	$⊢ (x = A \land y = B \land z = w) \to z = w$
10	6 8 9	breq123d	$⊢ (x = A \land y = B \land z = w) \to (y F (x) z \leftrightarrow B F (A) w)$
11	10	eloprabga	$⊢ (A \in V \land B \in W \land w \in V) \to (⟨⟨A, B⟩, w⟩ \in \{⟨⟨x, y⟩, z⟩ \| y F (x) z\} \leftrightarrow B F (A) w)$
12	5 11	mp3an3	$⊢ (A \in V \land B \in W) \to (⟨⟨A, B⟩, w⟩ \in \{⟨⟨x, y⟩, z⟩ \| y F (x) z\} \leftrightarrow B F (A) w)$
13	4 12	bitrid	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ uncurry F w \leftrightarrow B F (A) w)$
14	13	iotabidv	$⊢ (A \in V \land B \in W) \to (ι w \| ⟨A, B⟩ uncurry F w) = (ι w \| B F (A) w)$
15		df-ov	$⊢ A uncurry F B = uncurry F (⟨A, B⟩)$
16		df-fv	$⊢ uncurry F (⟨A, B⟩) = (ι w \| ⟨A, B⟩ uncurry F w)$
17	15 16	eqtri	$⊢ A uncurry F B = (ι w \| ⟨A, B⟩ uncurry F w)$
18		df-fv	$⊢ F (A) (B) = (ι w \| B F (A) w)$
19	14 17 18	3eqtr4g	$⊢ (A \in V \land B \in W) \to A uncurry F B = F (A) (B)$

Metamath Proof Explorer