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 8090

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 6625	. . . . 5 ⊢ (𝐹 Fn (𝐴 × 𝐵) → Fun 𝐹)
2		1stconst 8083	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V)
3		dff1o3 6817	. . . . . . 7 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ↔ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–onto→V ∧ Fun ^◡(1^st ↾ (V × {𝐶}))))
4	3	simprbi 502	. . . . . 6 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V → Fun ^◡(1^st ↾ (V × {𝐶})))
5	2, 4	syl 18	. . . . 5 ⊢ (𝐶 ∈ 𝐵 → Fun ^◡(1^st ↾ (V × {𝐶})))
6		funco 6565	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun ^◡(1^st ↾ (V × {𝐶}))) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
7	1, 5, 6	syl2an 607	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
8		dmco 6246	. . . . 5 ⊢ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹)
9		fndm 6628	. . . . . . . 8 ⊢ (𝐹 Fn (𝐴 × 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
10	9	adantr 485	. . . . . . 7 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
11	10	imaeq2d 6053	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)))
12		imacnvcnv 6197	. . . . . . . . 9 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵))
13		df-ima 5665	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵))
14		resres 5982	. . . . . . . . . 10 ⊢ ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
15	14	rneqi 5918	. . . . . . . . 9 ⊢ ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
16	12, 13, 15	3eqtri 2792	. . . . . . . 8 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
17		inxp 5809	. . . . . . . . . . . . 13 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵))
18		incom 4164	. . . . . . . . . . . . . . 15 ⊢ (V ∩ 𝐴) = (𝐴 ∩ V)
19		inv1 4355	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ V) = 𝐴
20	18, 19	eqtri 2788	. . . . . . . . . . . . . 14 ⊢ (V ∩ 𝐴) = 𝐴
21	20	xpeq1i 5678	. . . . . . . . . . . . 13 ⊢ ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
22	17, 21	eqtri 2788	. . . . . . . . . . . 12 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
23		snssi 4747	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → {𝐶} ⊆ 𝐵)
24		dfss2 3925	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∩ 𝐵) = {𝐶})
25	23, 24	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ({𝐶} ∩ 𝐵) = {𝐶})
26	25	xpeq2d 5682	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐵 → (𝐴 × ({𝐶} ∩ 𝐵)) = (𝐴 × {𝐶}))
27	22, 26	eqtrid 2812	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × {𝐶}))
28	27	reseq2d 5969	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = (1^st ↾ (𝐴 × {𝐶})))
29	28	rneqd 5919	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = ran (1^st ↾ (𝐴 × {𝐶})))
30		1stconst 8083	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴)
31		f1ofo 6818	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴)
32		forn 6785	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
33	30, 31, 32	3syl 19	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
34	29, 33	eqtrd 2800	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = 𝐴)
35	16, 34	eqtrid 2812	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
36	35	adantl 486	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
37	11, 36	eqtrd 2800	. . . . 5 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = 𝐴)
38	8, 37	eqtrid 2812	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴)
39		curry2.1	. . . . . 6 ⊢ 𝐺 = (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))
40	39	fneq1i 6622	. . . . 5 ⊢ (𝐺 Fn 𝐴 ↔ (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴)
41		df-fn 6528	. . . . 5 ⊢ ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴 ↔ (Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) ∧ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴))
42	40, 41	bitri 278	. . . 4 ⊢ (𝐺 Fn 𝐴 ↔ (Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) ∧ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴))
43	7, 38, 42	sylanbrc 594	. . 3 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 Fn 𝐴)
44		dffn5 6929	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
45	43, 44	sylib 221	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
46	39	fveq1i 6872	. . . . 5 ⊢ (𝐺‘𝑥) = ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥)
47		dff1o4 6819	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ↔ ((1^st ↾ (V × {𝐶})) Fn (V × {𝐶}) ∧ ^◡(1^st ↾ (V × {𝐶})) Fn V))
48	2, 47	sylib 221	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶})) Fn (V × {𝐶}) ∧ ^◡(1^st ↾ (V × {𝐶})) Fn V))
49	48	simprd 500	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → ^◡(1^st ↾ (V × {𝐶})) Fn V)
50		vex 3461	. . . . . . 7 ⊢ 𝑥 ∈ V
51		fvco2 6968	. . . . . . 7 ⊢ ((^◡(1^st ↾ (V × {𝐶})) Fn V ∧ 𝑥 ∈ V) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
52	49, 50, 51	sylancl 597	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
53	52	ad2antlr 739	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
54	46, 53	eqtrid 2812	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
55	2	adantr 485	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V)
56	50	a1i 11	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ V)
57		snidg 4622	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ {𝐶})
58	57	adantr 485	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ {𝐶})
59	56, 58	opelxpd 5691	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶}))
60	55, 59	jca 520	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ∧ ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶})))
61	50	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐵 → 𝑥 ∈ V)
62	61, 57	opelxpd 5691	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶}))
63	62	fvresd 6891	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
64	63	adantr 485	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
65		op1stg 7986	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
66	65	ancoms 463	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
67	64, 66	eqtrd 2800	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = 𝑥)
68		f1ocnvfv 7266	. . . . . . . 8 ⊢ (((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ∧ ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶})) → (((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = 𝑥 → (^◡(1^st ↾ (V × {𝐶}))‘𝑥) = ⟨𝑥, 𝐶⟩))
69	60, 67, 68	sylc 66	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (^◡(1^st ↾ (V × {𝐶}))‘𝑥) = ⟨𝑥, 𝐶⟩)
70	69	fveq2d 6875	. . . . . 6 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
71	70	adantll 726	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
72		df-ov 7403	. . . . 5 ⊢ (𝑥𝐹𝐶) = (𝐹‘⟨𝑥, 𝐶⟩)
73	71, 72	eqtr4di 2818	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝑥𝐹𝐶))
74	54, 73	eqtrd 2800	. . 3 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝑥𝐹𝐶))
75	74	mpteq2dva 5198	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))
76	45, 75	eqtrd 2800	1 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1563 ∈ wcel 2145 Vcvv 3457 ∩ cin 3906 ⊆ wss 3907 {csn 4585 ⟨cop 4591 ↦ cmpt 5186 × cxp 5650 ^◡ccnv 5651 dom cdm 5652 ran crn 5653 ↾ cres 5654 “ cima 5655 ∘ ccom 5656 Fun wfun 6519 Fn wfn 6520 –onto→wfo 6523 –1-1-onto→wf1o 6524 ‘cfv 6525 (class class class)co 7400 1^st c1st 7972

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pr 5395 ax-un 7722

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-ov 7403 df-1st 7974 df-2nd 7975

This theorem is referenced by: curry2f 8091 curry2val 8092

W3C validator