curry2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > curry2		Structured version Visualization version GIF version

Theorem curry2 8106

Description: Composition with ^◡(1^st ↾ (V × {𝐶})) turns any binary operation 𝐹 with a constant second operand into a function 𝐺 of the first operand only. This transformation is called "currying". (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008.)

**Hypothesis**
Ref	Expression
curry2.1	⊢ 𝐺 = (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))

**Assertion**
Ref	Expression
curry2	⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝐶 𝑥,𝐹 𝑥,𝐺

**Proof of Theorem curry2**
Step	Hyp	Ref	Expression
1		fnfun 6638	. . . . 5 ⊢ (𝐹 Fn (𝐴 × 𝐵) → Fun 𝐹)
2		1stconst 8099	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V)
3		dff1o3 6824	. . . . . . 7 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ↔ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–onto→V ∧ Fun ^◡(1^st ↾ (V × {𝐶}))))
4	3	simprbi 496	. . . . . 6 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V → Fun ^◡(1^st ↾ (V × {𝐶})))
5	2, 4	syl 17	. . . . 5 ⊢ (𝐶 ∈ 𝐵 → Fun ^◡(1^st ↾ (V × {𝐶})))
6		funco 6576	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun ^◡(1^st ↾ (V × {𝐶}))) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
7	1, 5, 6	syl2an 596	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
8		dmco 6243	. . . . 5 ⊢ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹)
9		fndm 6641	. . . . . . . 8 ⊢ (𝐹 Fn (𝐴 × 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
10	9	adantr 480	. . . . . . 7 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
11	10	imaeq2d 6047	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)))
12		imacnvcnv 6195	. . . . . . . . 9 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵))
13		df-ima 5667	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵))
14		resres 5979	. . . . . . . . . 10 ⊢ ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
15	14	rneqi 5917	. . . . . . . . 9 ⊢ ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
16	12, 13, 15	3eqtri 2762	. . . . . . . 8 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
17		inxp 5811	. . . . . . . . . . . . 13 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵))
18		incom 4184	. . . . . . . . . . . . . . 15 ⊢ (V ∩ 𝐴) = (𝐴 ∩ V)
19		inv1 4373	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ V) = 𝐴
20	18, 19	eqtri 2758	. . . . . . . . . . . . . 14 ⊢ (V ∩ 𝐴) = 𝐴
21	20	xpeq1i 5680	. . . . . . . . . . . . 13 ⊢ ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
22	17, 21	eqtri 2758	. . . . . . . . . . . 12 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
23		snssi 4784	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → {𝐶} ⊆ 𝐵)
24		dfss2 3944	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∩ 𝐵) = {𝐶})
25	23, 24	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ({𝐶} ∩ 𝐵) = {𝐶})
26	25	xpeq2d 5684	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐵 → (𝐴 × ({𝐶} ∩ 𝐵)) = (𝐴 × {𝐶}))
27	22, 26	eqtrid 2782	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × {𝐶}))
28	27	reseq2d 5966	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = (1^st ↾ (𝐴 × {𝐶})))
29	28	rneqd 5918	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = ran (1^st ↾ (𝐴 × {𝐶})))
30		1stconst 8099	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴)
31		f1ofo 6825	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴)
32		forn 6793	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
33	30, 31, 32	3syl 18	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
34	29, 33	eqtrd 2770	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = 𝐴)
35	16, 34	eqtrid 2782	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
36	35	adantl 481	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
37	11, 36	eqtrd 2770	. . . . 5 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = 𝐴)
38	8, 37	eqtrid 2782	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴)
39		curry2.1	. . . . . 6 ⊢ 𝐺 = (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))
40	39	fneq1i 6635	. . . . 5 ⊢ (𝐺 Fn 𝐴 ↔ (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴)
41		df-fn 6534	. . . . 5 ⊢ ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴 ↔ (Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) ∧ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴))
42	40, 41	bitri 275	. . . 4 ⊢ (𝐺 Fn 𝐴 ↔ (Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) ∧ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴))
43	7, 38, 42	sylanbrc 583	. . 3 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 Fn 𝐴)
44		dffn5 6937	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
45	43, 44	sylib 218	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
46	39	fveq1i 6877	. . . . 5 ⊢ (𝐺‘𝑥) = ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥)
47		dff1o4 6826	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ↔ ((1^st ↾ (V × {𝐶})) Fn (V × {𝐶}) ∧ ^◡(1^st ↾ (V × {𝐶})) Fn V))
48	2, 47	sylib 218	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶})) Fn (V × {𝐶}) ∧ ^◡(1^st ↾ (V × {𝐶})) Fn V))
49	48	simprd 495	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → ^◡(1^st ↾ (V × {𝐶})) Fn V)
50		vex 3463	. . . . . . 7 ⊢ 𝑥 ∈ V
51		fvco2 6976	. . . . . . 7 ⊢ ((^◡(1^st ↾ (V × {𝐶})) Fn V ∧ 𝑥 ∈ V) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
52	49, 50, 51	sylancl 586	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
53	52	ad2antlr 727	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
54	46, 53	eqtrid 2782	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
55	2	adantr 480	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V)
56	50	a1i 11	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ V)
57		snidg 4636	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ {𝐶})
58	57	adantr 480	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ {𝐶})
59	56, 58	opelxpd 5693	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶}))
60	55, 59	jca 511	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ∧ ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶})))
61	50	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐵 → 𝑥 ∈ V)
62	61, 57	opelxpd 5693	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶}))
63	62	fvresd 6896	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
64	63	adantr 480	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
65		op1stg 8000	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
66	65	ancoms 458	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
67	64, 66	eqtrd 2770	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = 𝑥)
68		f1ocnvfv 7271	. . . . . . . 8 ⊢ (((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ∧ ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶})) → (((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = 𝑥 → (^◡(1^st ↾ (V × {𝐶}))‘𝑥) = ⟨𝑥, 𝐶⟩))
69	60, 67, 68	sylc 65	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (^◡(1^st ↾ (V × {𝐶}))‘𝑥) = ⟨𝑥, 𝐶⟩)
70	69	fveq2d 6880	. . . . . 6 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
71	70	adantll 714	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
72		df-ov 7408	. . . . 5 ⊢ (𝑥𝐹𝐶) = (𝐹‘⟨𝑥, 𝐶⟩)
73	71, 72	eqtr4di 2788	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝑥𝐹𝐶))
74	54, 73	eqtrd 2770	. . 3 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝑥𝐹𝐶))
75	74	mpteq2dva 5214	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))
76	45, 75	eqtrd 2770	1 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 Vcvv 3459 ∩ cin 3925 ⊆ wss 3926 {csn 4601 ⟨cop 4607 ↦ cmpt 5201 × cxp 5652 ^◡ccnv 5653 dom cdm 5654 ran crn 5655 ↾ cres 5656 “ cima 5657 ∘ ccom 5658 Fun wfun 6525 Fn wfn 6526 –onto→wfo 6529 –1-1-onto→wf1o 6530 ‘cfv 6531 (class class class)co 7405 1^st c1st 7986

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402 ax-un 7729

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7408 df-1st 7988 df-2nd 7989

This theorem is referenced by: curry2f 8107 curry2val 8108

W3C validator