mpocurryd

Description: The currying of an operation given in maps-to notation, splitting the operation (function of two arguments) into a function of the first argument, producing a function over the second argument. (Contributed by AV, 27-Oct-2019)

	Ref	Expression
Hypotheses	mpocurryd.f	$⊢ F = (x \in X, y \in Y ⟼ C)$
	mpocurryd.c	$⊢ φ \to \forall x \in X \forall y \in Y C \in V$
	mpocurryd.n	$⊢ φ \to Y \neq \emptyset$
Assertion	mpocurryd	$⊢ φ \to curry F = (x \in X ⟼ (y \in Y ⟼ C))$

Proof

Step	Hyp	Ref	Expression
1		mpocurryd.f	$⊢ F = (x \in X, y \in Y ⟼ C)$
2		mpocurryd.c	$⊢ φ \to \forall x \in X \forall y \in Y C \in V$
3		mpocurryd.n	$⊢ φ \to Y \neq \emptyset$
4		df-cur	$⊢ curry F = (x \in dom dom F ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\})$
5	1	dmmpoga	$⊢ \forall x \in X \forall y \in Y C \in V \to dom F = X \times Y$
6	2 5	syl	$⊢ φ \to dom F = X \times Y$
7	6	dmeqd	$⊢ φ \to dom dom F = dom (X \times Y)$
8		dmxp	$⊢ Y \neq \emptyset \to dom (X \times Y) = X$
9	3 8	syl	$⊢ φ \to dom (X \times Y) = X$
10	7 9	eqtrd	$⊢ φ \to dom dom F = X$
11	10	mpteq1d	$⊢ φ \to (x \in dom dom F ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\}) = (x \in X ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\})$
12		df-mpt	$⊢ (y \in Y ⟼ C) = \{⟨y, z⟩ \| (y \in Y \land z = C)\}$
13	1	mpofun	$⊢ Fun F$
14		funbrfv2b	$⊢ Fun F \to (⟨x, y⟩ F z \leftrightarrow (⟨x, y⟩ \in dom F \land F (⟨x, y⟩) = z))$
15	13 14	mp1i	$⊢ (φ \land x \in X) \to (⟨x, y⟩ F z \leftrightarrow (⟨x, y⟩ \in dom F \land F (⟨x, y⟩) = z))$
16	6	adantr	$⊢ (φ \land x \in X) \to dom F = X \times Y$
17	16	eleq2d	$⊢ (φ \land x \in X) \to (⟨x, y⟩ \in dom F \leftrightarrow ⟨x, y⟩ \in (X \times Y))$
18		opelxp	$⊢ ⟨x, y⟩ \in (X \times Y) \leftrightarrow (x \in X \land y \in Y)$
19	17 18	bitrdi	$⊢ (φ \land x \in X) \to (⟨x, y⟩ \in dom F \leftrightarrow (x \in X \land y \in Y))$
20	19	anbi1d	$⊢ (φ \land x \in X) \to ((⟨x, y⟩ \in dom F \land F (⟨x, y⟩) = z) \leftrightarrow ((x \in X \land y \in Y) \land F (⟨x, y⟩) = z))$
21		an21	$⊢ ((x \in X \land y \in Y) \land F (⟨x, y⟩) = z) \leftrightarrow (y \in Y \land (x \in X \land F (⟨x, y⟩) = z))$
22		ibar	$⊢ x \in X \to (F (⟨x, y⟩) = z \leftrightarrow (x \in X \land F (⟨x, y⟩) = z))$
23	22	bicomd	$⊢ x \in X \to ((x \in X \land F (⟨x, y⟩) = z) \leftrightarrow F (⟨x, y⟩) = z)$
24	23	adantl	$⊢ (φ \land x \in X) \to ((x \in X \land F (⟨x, y⟩) = z) \leftrightarrow F (⟨x, y⟩) = z)$
25	24	adantr	$⊢ ((φ \land x \in X) \land y \in Y) \to ((x \in X \land F (⟨x, y⟩) = z) \leftrightarrow F (⟨x, y⟩) = z)$
26		df-ov	$⊢ x F y = F (⟨x, y⟩)$
27		nfcv	$⊢ \underline{Ⅎ} a C$
28		nfcv	$⊢ \underline{Ⅎ} b C$
29		nfcv	$⊢ \underline{Ⅎ} x b$
30		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ C$
31	29 30	nfcsbw	$⊢ \underline{Ⅎ} x ⦋ b / y ⦌ ⦋ a / x ⦌ C$
32		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ b / y ⦌ ⦋ a / x ⦌ C$
33		csbeq1a	$⊢ x = a \to C = ⦋ a / x ⦌ C$
34		csbeq1a	$⊢ y = b \to ⦋ a / x ⦌ C = ⦋ b / y ⦌ ⦋ a / x ⦌ C$
35	33 34	sylan9eq	$⊢ (x = a \land y = b) \to C = ⦋ b / y ⦌ ⦋ a / x ⦌ C$
36	27 28 31 32 35	cbvmpo	$⊢ (x \in X, y \in Y ⟼ C) = (a \in X, b \in Y ⟼ ⦋ b / y ⦌ ⦋ a / x ⦌ C)$
37	1 36	eqtri	$⊢ F = (a \in X, b \in Y ⟼ ⦋ b / y ⦌ ⦋ a / x ⦌ C)$
38	37	a1i	$⊢ ((φ \land x \in X) \land y \in Y) \to F = (a \in X, b \in Y ⟼ ⦋ b / y ⦌ ⦋ a / x ⦌ C)$
39	33	eqcomd	$⊢ x = a \to ⦋ a / x ⦌ C = C$
40	39	equcoms	$⊢ a = x \to ⦋ a / x ⦌ C = C$
41	40	csbeq2dv	$⊢ a = x \to ⦋ b / y ⦌ ⦋ a / x ⦌ C = ⦋ b / y ⦌ C$
42		csbeq1a	$⊢ y = b \to C = ⦋ b / y ⦌ C$
43	42	eqcomd	$⊢ y = b \to ⦋ b / y ⦌ C = C$
44	43	equcoms	$⊢ b = y \to ⦋ b / y ⦌ C = C$
45	41 44	sylan9eq	$⊢ (a = x \land b = y) \to ⦋ b / y ⦌ ⦋ a / x ⦌ C = C$
46	45	adantl	$⊢ (((φ \land x \in X) \land y \in Y) \land (a = x \land b = y)) \to ⦋ b / y ⦌ ⦋ a / x ⦌ C = C$
47		simpr	$⊢ (φ \land x \in X) \to x \in X$
48	47	adantr	$⊢ ((φ \land x \in X) \land y \in Y) \to x \in X$
49		simpr	$⊢ ((φ \land x \in X) \land y \in Y) \to y \in Y$
50		rsp2	$⊢ \forall x \in X \forall y \in Y C \in V \to ((x \in X \land y \in Y) \to C \in V)$
51	2 50	syl	$⊢ φ \to ((x \in X \land y \in Y) \to C \in V)$
52	51	impl	$⊢ ((φ \land x \in X) \land y \in Y) \to C \in V$
53	38 46 48 49 52	ovmpod	$⊢ ((φ \land x \in X) \land y \in Y) \to x F y = C$
54	26 53	eqtr3id	$⊢ ((φ \land x \in X) \land y \in Y) \to F (⟨x, y⟩) = C$
55	54	eqeq1d	$⊢ ((φ \land x \in X) \land y \in Y) \to (F (⟨x, y⟩) = z \leftrightarrow C = z)$
56		eqcom	$⊢ C = z \leftrightarrow z = C$
57	55 56	bitrdi	$⊢ ((φ \land x \in X) \land y \in Y) \to (F (⟨x, y⟩) = z \leftrightarrow z = C)$
58	25 57	bitrd	$⊢ ((φ \land x \in X) \land y \in Y) \to ((x \in X \land F (⟨x, y⟩) = z) \leftrightarrow z = C)$
59	58	pm5.32da	$⊢ (φ \land x \in X) \to ((y \in Y \land (x \in X \land F (⟨x, y⟩) = z)) \leftrightarrow (y \in Y \land z = C))$
60	21 59	syl5bb	$⊢ (φ \land x \in X) \to (((x \in X \land y \in Y) \land F (⟨x, y⟩) = z) \leftrightarrow (y \in Y \land z = C))$
61	15 20 60	3bitrrd	$⊢ (φ \land x \in X) \to ((y \in Y \land z = C) \leftrightarrow ⟨x, y⟩ F z)$
62	61	opabbidv	$⊢ (φ \land x \in X) \to \{⟨y, z⟩ \| (y \in Y \land z = C)\} = \{⟨y, z⟩ \| ⟨x, y⟩ F z\}$
63	12 62	eqtr2id	$⊢ (φ \land x \in X) \to \{⟨y, z⟩ \| ⟨x, y⟩ F z\} = (y \in Y ⟼ C)$
64	63	mpteq2dva	$⊢ φ \to (x \in X ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\}) = (x \in X ⟼ (y \in Y ⟼ C))$
65	11 64	eqtrd	$⊢ φ \to (x \in dom dom F ⟼ \{⟨y, z⟩ \| ⟨x, y⟩ F z\}) = (x \in X ⟼ (y \in Y ⟼ C))$
66	4 65	eqtrid	$⊢ φ \to curry F = (x \in X ⟼ (y \in Y ⟼ C))$

Metamath Proof Explorer

Theorem mpocurryd

Proof