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 7918

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 6517	. . . . 5 ⊢ (𝐹 Fn (𝐴 × 𝐵) → Fun 𝐹)
2		1stconst 7911	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V)
3		dff1o3 6706	. . . . . . 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 6458	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun ^◡(1^st ↾ (V × {𝐶}))) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
7	1, 5, 6	syl2an 595	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
8		dmco 6147	. . . . 5 ⊢ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹)
9		fndm 6520	. . . . . . . 8 ⊢ (𝐹 Fn (𝐴 × 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
10	9	adantr 480	. . . . . . 7 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
11	10	imaeq2d 5958	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)))
12		imacnvcnv 6098	. . . . . . . . 9 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵))
13		df-ima 5593	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵))
14		resres 5893	. . . . . . . . . 10 ⊢ ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
15	14	rneqi 5835	. . . . . . . . 9 ⊢ ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
16	12, 13, 15	3eqtri 2770	. . . . . . . 8 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
17		inxp 5730	. . . . . . . . . . . . 13 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵))
18		incom 4131	. . . . . . . . . . . . . . 15 ⊢ (V ∩ 𝐴) = (𝐴 ∩ V)
19		inv1 4325	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ V) = 𝐴
20	18, 19	eqtri 2766	. . . . . . . . . . . . . 14 ⊢ (V ∩ 𝐴) = 𝐴
21	20	xpeq1i 5606	. . . . . . . . . . . . 13 ⊢ ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
22	17, 21	eqtri 2766	. . . . . . . . . . . 12 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
23		snssi 4738	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → {𝐶} ⊆ 𝐵)
24		df-ss 3900	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∩ 𝐵) = {𝐶})
25	23, 24	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ({𝐶} ∩ 𝐵) = {𝐶})
26	25	xpeq2d 5610	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐵 → (𝐴 × ({𝐶} ∩ 𝐵)) = (𝐴 × {𝐶}))
27	22, 26	eqtrid 2790	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × {𝐶}))
28	27	reseq2d 5880	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = (1^st ↾ (𝐴 × {𝐶})))
29	28	rneqd 5836	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = ran (1^st ↾ (𝐴 × {𝐶})))
30		1stconst 7911	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴)
31		f1ofo 6707	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴)
32		forn 6675	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
33	30, 31, 32	3syl 18	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
34	29, 33	eqtrd 2778	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = 𝐴)
35	16, 34	eqtrid 2790	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
36	35	adantl 481	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
37	11, 36	eqtrd 2778	. . . . 5 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = 𝐴)
38	8, 37	eqtrid 2790	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴)
39		curry2.1	. . . . . 6 ⊢ 𝐺 = (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))
40	39	fneq1i 6514	. . . . 5 ⊢ (𝐺 Fn 𝐴 ↔ (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴)
41		df-fn 6421	. . . . 5 ⊢ ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴 ↔ (Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) ∧ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴))
42	40, 41	bitri 274	. . . 4 ⊢ (𝐺 Fn 𝐴 ↔ (Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) ∧ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴))
43	7, 38, 42	sylanbrc 582	. . 3 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 Fn 𝐴)
44		dffn5 6810	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
45	43, 44	sylib 217	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
46	39	fveq1i 6757	. . . . 5 ⊢ (𝐺‘𝑥) = ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥)
47		dff1o4 6708	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ↔ ((1^st ↾ (V × {𝐶})) Fn (V × {𝐶}) ∧ ^◡(1^st ↾ (V × {𝐶})) Fn V))
48	2, 47	sylib 217	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶})) Fn (V × {𝐶}) ∧ ^◡(1^st ↾ (V × {𝐶})) Fn V))
49	48	simprd 495	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → ^◡(1^st ↾ (V × {𝐶})) Fn V)
50		vex 3426	. . . . . . 7 ⊢ 𝑥 ∈ V
51		fvco2 6847	. . . . . . 7 ⊢ ((^◡(1^st ↾ (V × {𝐶})) Fn V ∧ 𝑥 ∈ V) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
52	49, 50, 51	sylancl 585	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
53	52	ad2antlr 723	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
54	46, 53	eqtrid 2790	. . . 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 4592	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ {𝐶})
58	57	adantr 480	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ {𝐶})
59	56, 58	opelxpd 5618	. . . . . . . . 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 5618	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶}))
63	62	fvresd 6776	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
64	63	adantr 480	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
65		op1stg 7816	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
66	65	ancoms 458	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
67	64, 66	eqtrd 2778	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = 𝑥)
68		f1ocnvfv 7131	. . . . . . . 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 6760	. . . . . 6 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
71	70	adantll 710	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
72		df-ov 7258	. . . . 5 ⊢ (𝑥𝐹𝐶) = (𝐹‘⟨𝑥, 𝐶⟩)
73	71, 72	eqtr4di 2797	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝑥𝐹𝐶))
74	54, 73	eqtrd 2778	. . 3 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝑥𝐹𝐶))
75	74	mpteq2dva 5170	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))
76	45, 75	eqtrd 2778	1 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2108 Vcvv 3422 ∩ cin 3882 ⊆ wss 3883 {csn 4558 ⟨cop 4564 ↦ cmpt 5153 × cxp 5578 ^◡ccnv 5579 dom cdm 5580 ran crn 5581 ↾ cres 5582 “ cima 5583 ∘ ccom 5584 Fun wfun 6412 Fn wfn 6413 –onto→wfo 6416 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 1^st c1st 7802

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-ov 7258 df-1st 7804 df-2nd 7805

This theorem is referenced by: curry2f 7919 curry2val 7920

W3C validator