curf

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

		Ref	Expression
	Assertion	curf	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to curry F : A ⟶ C^{B}$

Proof

Step	Hyp	Ref	Expression
1		opelxpi	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in (A \times B)$
2		ffvelrn	$⊢ (F : A \times B ⟶ C \land ⟨x, y⟩ \in (A \times B)) \to F (⟨x, y⟩) \in C$
3	1 2	sylan2	$⊢ (F : A \times B ⟶ C \land (x \in A \land y \in B)) \to F (⟨x, y⟩) \in C$
4	3	anassrs	$⊢ ((F : A \times B ⟶ C \land x \in A) \land y \in B) \to F (⟨x, y⟩) \in C$
5	4	fmpttd	$⊢ (F : A \times B ⟶ C \land x \in A) \to (y \in B ⟼ F (⟨x, y⟩)) : B ⟶ C$
6	5	3ad2antl1	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land x \in A) \to (y \in B ⟼ F (⟨x, y⟩)) : B ⟶ C$
7		elmapg	$⊢ (C \in W \land B \in (V ∖ \{\emptyset\})) \to ((y \in B ⟼ F (⟨x, y⟩)) \in (C^{B}) \leftrightarrow (y \in B ⟼ F (⟨x, y⟩)) : B ⟶ C)$
8	7	ancoms	$⊢ (B \in (V ∖ \{\emptyset\}) \land C \in W) \to ((y \in B ⟼ F (⟨x, y⟩)) \in (C^{B}) \leftrightarrow (y \in B ⟼ F (⟨x, y⟩)) : B ⟶ C)$
9	8	3adant1	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to ((y \in B ⟼ F (⟨x, y⟩)) \in (C^{B}) \leftrightarrow (y \in B ⟼ F (⟨x, y⟩)) : B ⟶ C)$
10	9	adantr	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land x \in A) \to ((y \in B ⟼ F (⟨x, y⟩)) \in (C^{B}) \leftrightarrow (y \in B ⟼ F (⟨x, y⟩)) : B ⟶ C)$
11	6 10	mpbird	$⊢ ((F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \land x \in A) \to (y \in B ⟼ F (⟨x, y⟩)) \in (C^{B})$
12	11	fmpttd	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to (x \in A ⟼ (y \in B ⟼ F (⟨x, y⟩))) : A ⟶ C^{B}$
13		eldifsni	$⊢ B \in (V ∖ \{\emptyset\}) \to B \neq \emptyset$
14		df-cur	$⊢ curry F = (x \in dom dom F ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\})$
15		fdm	$⊢ F : A \times B ⟶ C \to dom F = A \times B$
16	15	dmeqd	$⊢ F : A \times B ⟶ C \to dom dom F = dom (A \times B)$
17		dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$
18	16 17	sylan9eq	$⊢ (F : A \times B ⟶ C \land B \neq \emptyset) \to dom dom F = A$
19	18	mpteq1d	$⊢ (F : A \times B ⟶ C \land B \neq \emptyset) \to (x \in dom dom F ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\}) = (x \in A ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\})$
20		ffun	$⊢ F : A \times B ⟶ C \to Fun F$
21		funbrfv2b	$⊢ Fun F \to (⟨x, y⟩ F z \leftrightarrow (⟨x, y⟩ \in dom F \land F (⟨x, y⟩) = z))$
22	20 21	syl	$⊢ F : A \times B ⟶ C \to (⟨x, y⟩ F z \leftrightarrow (⟨x, y⟩ \in dom F \land F (⟨x, y⟩) = z))$
23	15	eleq2d	$⊢ F : A \times B ⟶ C \to (⟨x, y⟩ \in dom F \leftrightarrow ⟨x, y⟩ \in (A \times B))$
24		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
25	23 24	syl6bb	$⊢ F : A \times B ⟶ C \to (⟨x, y⟩ \in dom F \leftrightarrow (x \in A \land y \in B))$
26	25	anbi1d	$⊢ F : A \times B ⟶ C \to ((⟨x, y⟩ \in dom F \land F (⟨x, y⟩) = z) \leftrightarrow ((x \in A \land y \in B) \land F (⟨x, y⟩) = z))$
27	22 26	bitrd	$⊢ F : A \times B ⟶ C \to (⟨x, y⟩ F z \leftrightarrow ((x \in A \land y \in B) \land F (⟨x, y⟩) = z))$
28		ibar	$⊢ x \in A \to ((y \in B \land z = F (⟨x, y⟩)) \leftrightarrow (x \in A \land (y \in B \land z = F (⟨x, y⟩))))$
29		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⟩)))$
30		eqcom	$⊢ z = F (⟨x, y⟩) \leftrightarrow F (⟨x, y⟩) = z$
31	30	anbi2i	$⊢ ((x \in A \land y \in B) \land z = F (⟨x, y⟩)) \leftrightarrow ((x \in A \land y \in B) \land F (⟨x, y⟩) = z)$
32	29 31	bitr3i	$⊢ (x \in A \land (y \in B \land z = F (⟨x, y⟩))) \leftrightarrow ((x \in A \land y \in B) \land F (⟨x, y⟩) = z)$
33	28 32	bitr2di	$⊢ x \in A \to (((x \in A \land y \in B) \land F (⟨x, y⟩) = z) \leftrightarrow (y \in B \land z = F (⟨x, y⟩)))$
34	27 33	sylan9bb	$⊢ (F : A \times B ⟶ C \land x \in A) \to (⟨x, y⟩ F z \leftrightarrow (y \in B \land z = F (⟨x, y⟩)))$
35	34	opabbidv	$⊢ (F : A \times B ⟶ C \land x \in A) \to \{⟨y, z⟩ \| ⟨x, y⟩ F z\} = \{⟨y, z⟩ \| (y \in B \land z = F (⟨x, y⟩))\}$
36		df-mpt	$⊢ (y \in B ⟼ F (⟨x, y⟩)) = \{⟨y, z⟩ \| (y \in B \land z = F (⟨x, y⟩))\}$
37	35 36	eqtr4di	$⊢ (F : A \times B ⟶ C \land x \in A) \to \{⟨y, z⟩ \| ⟨x, y⟩ F z\} = (y \in B ⟼ F (⟨x, y⟩))$
38	37	mpteq2dva	$⊢ F : A \times B ⟶ C \to (x \in A ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\}) = (x \in A ⟼ (y \in B ⟼ F (⟨x, y⟩)))$
39	38	adantr	$⊢ (F : A \times B ⟶ C \land B \neq \emptyset) \to (x \in A ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\}) = (x \in A ⟼ (y \in B ⟼ F (⟨x, y⟩)))$
40	19 39	eqtrd	$⊢ (F : A \times B ⟶ C \land B \neq \emptyset) \to (x \in dom dom F ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\}) = (x \in A ⟼ (y \in B ⟼ F (⟨x, y⟩)))$
41	14 40	syl5eq	$⊢ (F : A \times B ⟶ C \land B \neq \emptyset) \to curry F = (x \in A ⟼ (y \in B ⟼ F (⟨x, y⟩)))$
42	41	feq1d	$⊢ (F : A \times B ⟶ C \land B \neq \emptyset) \to (curry F : A ⟶ C^{B} \leftrightarrow (x \in A ⟼ (y \in B ⟼ F (⟨x, y⟩))) : A ⟶ C^{B})$
43	13 42	sylan2	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\})) \to (curry F : A ⟶ C^{B} \leftrightarrow (x \in A ⟼ (y \in B ⟼ F (⟨x, y⟩))) : A ⟶ C^{B})$
44	43	3adant3	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to (curry F : A ⟶ C^{B} \leftrightarrow (x \in A ⟼ (y \in B ⟼ F (⟨x, y⟩))) : A ⟶ C^{B})$
45	12 44	mpbird	$⊢ (F : A \times B ⟶ C \land B \in (V ∖ \{\emptyset\}) \land C \in W) \to curry F : A ⟶ C^{B}$

Metamath Proof Explorer

Theorem curf

Proof