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 8059

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 6600	. . . . 5 ⊢ (𝐹 Fn (𝐴 × 𝐵) → Fun 𝐹)
2		1stconst 8052	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V)
3		dff1o3 6788	. . . . . . 7 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ↔ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–onto→V ∧ Fun ^◡(1^st ↾ (V × {𝐶}))))
4	3	simprbi 497	. . . . . 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 6540	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun ^◡(1^st ↾ (V × {𝐶}))) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
7	1, 5, 6	syl2an 597	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
8		dmco 6221	. . . . 5 ⊢ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹)
9		fndm 6603	. . . . . . . 8 ⊢ (𝐹 Fn (𝐴 × 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
10	9	adantr 480	. . . . . . 7 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
11	10	imaeq2d 6027	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)))
12		imacnvcnv 6172	. . . . . . . . 9 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵))
13		df-ima 5645	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵))
14		resres 5959	. . . . . . . . . 10 ⊢ ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
15	14	rneqi 5894	. . . . . . . . 9 ⊢ ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
16	12, 13, 15	3eqtri 2764	. . . . . . . 8 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
17		inxp 5788	. . . . . . . . . . . . 13 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵))
18		incom 4163	. . . . . . . . . . . . . . 15 ⊢ (V ∩ 𝐴) = (𝐴 ∩ V)
19		inv1 4352	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ V) = 𝐴
20	18, 19	eqtri 2760	. . . . . . . . . . . . . 14 ⊢ (V ∩ 𝐴) = 𝐴
21	20	xpeq1i 5658	. . . . . . . . . . . . 13 ⊢ ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
22	17, 21	eqtri 2760	. . . . . . . . . . . 12 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
23		snssi 4766	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → {𝐶} ⊆ 𝐵)
24		dfss2 3921	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∩ 𝐵) = {𝐶})
25	23, 24	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ({𝐶} ∩ 𝐵) = {𝐶})
26	25	xpeq2d 5662	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐵 → (𝐴 × ({𝐶} ∩ 𝐵)) = (𝐴 × {𝐶}))
27	22, 26	eqtrid 2784	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × {𝐶}))
28	27	reseq2d 5946	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = (1^st ↾ (𝐴 × {𝐶})))
29	28	rneqd 5895	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = ran (1^st ↾ (𝐴 × {𝐶})))
30		1stconst 8052	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴)
31		f1ofo 6789	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴)
32		forn 6757	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
33	30, 31, 32	3syl 18	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
34	29, 33	eqtrd 2772	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = 𝐴)
35	16, 34	eqtrid 2784	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
36	35	adantl 481	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
37	11, 36	eqtrd 2772	. . . . 5 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = 𝐴)
38	8, 37	eqtrid 2784	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴)
39		curry2.1	. . . . . 6 ⊢ 𝐺 = (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))
40	39	fneq1i 6597	. . . . 5 ⊢ (𝐺 Fn 𝐴 ↔ (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴)
41		df-fn 6503	. . . . 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 584	. . 3 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 Fn 𝐴)
44		dffn5 6900	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
45	43, 44	sylib 218	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
46	39	fveq1i 6843	. . . . 5 ⊢ (𝐺‘𝑥) = ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥)
47		dff1o4 6790	. . . . . . . . 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 3446	. . . . . . 7 ⊢ 𝑥 ∈ V
51		fvco2 6939	. . . . . . 7 ⊢ ((^◡(1^st ↾ (V × {𝐶})) Fn V ∧ 𝑥 ∈ V) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
52	49, 50, 51	sylancl 587	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
53	52	ad2antlr 728	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
54	46, 53	eqtrid 2784	. . . 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 4619	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ {𝐶})
58	57	adantr 480	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ {𝐶})
59	56, 58	opelxpd 5671	. . . . . . . . 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 5671	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶}))
63	62	fvresd 6862	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
64	63	adantr 480	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
65		op1stg 7955	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
66	65	ancoms 458	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
67	64, 66	eqtrd 2772	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = 𝑥)
68		f1ocnvfv 7234	. . . . . . . 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 6846	. . . . . 6 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
71	70	adantll 715	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
72		df-ov 7371	. . . . 5 ⊢ (𝑥𝐹𝐶) = (𝐹‘⟨𝑥, 𝐶⟩)
73	71, 72	eqtr4di 2790	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝑥𝐹𝐶))
74	54, 73	eqtrd 2772	. . 3 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝑥𝐹𝐶))
75	74	mpteq2dva 5193	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))
76	45, 75	eqtrd 2772	1 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 Vcvv 3442 ∩ cin 3902 ⊆ wss 3903 {csn 4582 ⟨cop 4588 ↦ cmpt 5181 × cxp 5630 ^◡ccnv 5631 dom cdm 5632 ran crn 5633 ↾ cres 5634 “ cima 5635 ∘ ccom 5636 Fun wfun 6494 Fn wfn 6495 –onto→wfo 6498 –1-1-onto→wf1o 6499 ‘cfv 6500 (class class class)co 7368 1^st c1st 7941

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pr 5379 ax-un 7690

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7371 df-1st 7943 df-2nd 7944

This theorem is referenced by: curry2f 8060 curry2val 8061

W3C validator