uncf

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

		Ref	Expression
	Assertion	uncf	$⊢ F : A ⟶ C^{B} \to uncurry F : A \times B ⟶ C$

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	$⊢ (F : A ⟶ C^{B} \land x \in A) \to F (x) \in (C^{B})$
2		elmapi	$⊢ F (x) \in (C^{B}) \to F (x) : B ⟶ C$
3	1 2	syl	$⊢ (F : A ⟶ C^{B} \land x \in A) \to F (x) : B ⟶ C$
4	3	ffvelrnda	$⊢ ((F : A ⟶ C^{B} \land x \in A) \land y \in B) \to F (x) (y) \in C$
5	4	anasss	$⊢ (F : A ⟶ C^{B} \land (x \in A \land y \in B)) \to F (x) (y) \in C$
6	5	ralrimivva	$⊢ F : A ⟶ C^{B} \to \forall x \in A \forall y \in B F (x) (y) \in C$
7		df-unc	$⊢ uncurry F = \{⟨⟨x, y⟩, z⟩ \| y F (x) z\}$
8		df-br	$⊢ y F (x) z \leftrightarrow ⟨y, z⟩ \in F (x)$
9		elfvdm	$⊢ ⟨y, z⟩ \in F (x) \to x \in dom F$
10	8 9	sylbi	$⊢ y F (x) z \to x \in dom F$
11		fdm	$⊢ F : A ⟶ C^{B} \to dom F = A$
12	11	eleq2d	$⊢ F : A ⟶ C^{B} \to (x \in dom F \leftrightarrow x \in A)$
13	10 12	syl5ib	$⊢ F : A ⟶ C^{B} \to (y F (x) z \to x \in A)$
14	13	pm4.71rd	$⊢ F : A ⟶ C^{B} \to (y F (x) z \leftrightarrow (x \in A \land y F (x) z))$
15		elmapfun	$⊢ F (x) \in (C^{B}) \to Fun F (x)$
16		funbrfv2b	$⊢ Fun F (x) \to (y F (x) z \leftrightarrow (y \in dom F (x) \land F (x) (y) = z))$
17	1 15 16	3syl	$⊢ (F : A ⟶ C^{B} \land x \in A) \to (y F (x) z \leftrightarrow (y \in dom F (x) \land F (x) (y) = z))$
18		fdm	$⊢ F (x) : B ⟶ C \to dom F (x) = B$
19	1 2 18	3syl	$⊢ (F : A ⟶ C^{B} \land x \in A) \to dom F (x) = B$
20	19	eleq2d	$⊢ (F : A ⟶ C^{B} \land x \in A) \to (y \in dom F (x) \leftrightarrow y \in B)$
21		eqcom	$⊢ F (x) (y) = z \leftrightarrow z = F (x) (y)$
22	21	a1i	$⊢ (F : A ⟶ C^{B} \land x \in A) \to (F (x) (y) = z \leftrightarrow z = F (x) (y))$
23	20 22	anbi12d	$⊢ (F : A ⟶ C^{B} \land x \in A) \to ((y \in dom F (x) \land F (x) (y) = z) \leftrightarrow (y \in B \land z = F (x) (y)))$
24	17 23	bitrd	$⊢ (F : A ⟶ C^{B} \land x \in A) \to (y F (x) z \leftrightarrow (y \in B \land z = F (x) (y)))$
25	24	pm5.32da	$⊢ F : A ⟶ C^{B} \to ((x \in A \land y F (x) z) \leftrightarrow (x \in A \land (y \in B \land z = F (x) (y))))$
26	14 25	bitrd	$⊢ F : A ⟶ C^{B} \to (y F (x) z \leftrightarrow (x \in A \land (y \in B \land z = F (x) (y))))$
27		anass	$⊢ ((x \in A \land y \in B) \land z = F (x) (y)) \leftrightarrow (x \in A \land (y \in B \land z = F (x) (y)))$
28	26 27	bitr4di	$⊢ F : A ⟶ C^{B} \to (y F (x) z \leftrightarrow ((x \in A \land y \in B) \land z = F (x) (y)))$
29	28	oprabbidv	$⊢ F : A ⟶ C^{B} \to \{⟨⟨x, y⟩, z⟩ \| y F (x) z\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = F (x) (y))\}$
30	7 29	syl5eq	$⊢ F : A ⟶ C^{B} \to uncurry F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = F (x) (y))\}$
31	30	feq1d	$⊢ F : A ⟶ C^{B} \to (uncurry F : A \times B ⟶ C \leftrightarrow \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = F (x) (y))\} : A \times B ⟶ C)$
32		df-mpo	$⊢ (x \in A, y \in B ⟼ F (x) (y)) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = F (x) (y))\}$
33	32	eqcomi	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = F (x) (y))\} = (x \in A, y \in B ⟼ F (x) (y))$
34	33	fmpo	$⊢ \forall x \in A \forall y \in B F (x) (y) \in C \leftrightarrow \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = F (x) (y))\} : A \times B ⟶ C$
35	31 34	bitr4di	$⊢ F : A ⟶ C^{B} \to (uncurry F : A \times B ⟶ C \leftrightarrow \forall x \in A \forall y \in B F (x) (y) \in C)$
36	6 35	mpbird	$⊢ F : A ⟶ C^{B} \to uncurry F : A \times B ⟶ C$

Metamath Proof Explorer

Theorem uncf

Proof