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 7794

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 6446	. . . . 5 ⊢ (𝐹 Fn (𝐴 × 𝐵) → Fun 𝐹)
2		1stconst 7787	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V)
3		dff1o3 6614	. . . . . . 7 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ↔ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–onto→V ∧ Fun ^◡(1^st ↾ (V × {𝐶}))))
4	3	simprbi 499	. . . . . 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 6388	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun ^◡(1^st ↾ (V × {𝐶}))) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
7	1, 5, 6	syl2an 597	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))))
8		dmco 6100	. . . . 5 ⊢ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹)
9		fndm 6448	. . . . . . . 8 ⊢ (𝐹 Fn (𝐴 × 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
10	9	adantr 483	. . . . . . 7 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
11	10	imaeq2d 5922	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)))
12		imacnvcnv 6056	. . . . . . . . 9 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵))
13		df-ima 5561	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵))
14		resres 5859	. . . . . . . . . 10 ⊢ ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
15	14	rneqi 5800	. . . . . . . . 9 ⊢ ran ((1^st ↾ (V × {𝐶})) ↾ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
16	12, 13, 15	3eqtri 2846	. . . . . . . 8 ⊢ (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵)))
17		inxp 5696	. . . . . . . . . . . . 13 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵))
18		incom 4176	. . . . . . . . . . . . . . 15 ⊢ (V ∩ 𝐴) = (𝐴 ∩ V)
19		inv1 4346	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ V) = 𝐴
20	18, 19	eqtri 2842	. . . . . . . . . . . . . 14 ⊢ (V ∩ 𝐴) = 𝐴
21	20	xpeq1i 5574	. . . . . . . . . . . . 13 ⊢ ((V ∩ 𝐴) × ({𝐶} ∩ 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
22	17, 21	eqtri 2842	. . . . . . . . . . . 12 ⊢ ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × ({𝐶} ∩ 𝐵))
23		snssi 4733	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → {𝐶} ⊆ 𝐵)
24		df-ss 3950	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∩ 𝐵) = {𝐶})
25	23, 24	sylib 220	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ({𝐶} ∩ 𝐵) = {𝐶})
26	25	xpeq2d 5578	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐵 → (𝐴 × ({𝐶} ∩ 𝐵)) = (𝐴 × {𝐶}))
27	22, 26	syl5eq 2866	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ((V × {𝐶}) ∩ (𝐴 × 𝐵)) = (𝐴 × {𝐶}))
28	27	reseq2d 5846	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = (1^st ↾ (𝐴 × {𝐶})))
29	28	rneqd 5801	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = ran (1^st ↾ (𝐴 × {𝐶})))
30		1stconst 7787	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴)
31		f1ofo 6615	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–1-1-onto→𝐴 → (1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴)
32		forn 6586	. . . . . . . . . 10 ⊢ ((1^st ↾ (𝐴 × {𝐶})):(𝐴 × {𝐶})–onto→𝐴 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
33	30, 31, 32	3syl 18	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ (𝐴 × {𝐶})) = 𝐴)
34	29, 33	eqtrd 2854	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ran (1^st ↾ ((V × {𝐶}) ∩ (𝐴 × 𝐵))) = 𝐴)
35	16, 34	syl5eq 2866	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
36	35	adantl 484	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ (𝐴 × 𝐵)) = 𝐴)
37	11, 36	eqtrd 2854	. . . . 5 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (^◡^◡(1^st ↾ (V × {𝐶})) “ dom 𝐹) = 𝐴)
38	8, 37	syl5eq 2866	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴)
39		curry2.1	. . . . . 6 ⊢ 𝐺 = (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))
40	39	fneq1i 6443	. . . . 5 ⊢ (𝐺 Fn 𝐴 ↔ (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴)
41		df-fn 6351	. . . . 5 ⊢ ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) Fn 𝐴 ↔ (Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) ∧ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴))
42	40, 41	bitri 277	. . . 4 ⊢ (𝐺 Fn 𝐴 ↔ (Fun (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) ∧ dom (𝐹 ∘ ^◡(1^st ↾ (V × {𝐶}))) = 𝐴))
43	7, 38, 42	sylanbrc 585	. . 3 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 Fn 𝐴)
44		dffn5 6717	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
45	43, 44	sylib 220	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
46	39	fveq1i 6664	. . . . 5 ⊢ (𝐺‘𝑥) = ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥)
47		dff1o4 6616	. . . . . . . . 9 ⊢ ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ↔ ((1^st ↾ (V × {𝐶})) Fn (V × {𝐶}) ∧ ^◡(1^st ↾ (V × {𝐶})) Fn V))
48	2, 47	sylib 220	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶})) Fn (V × {𝐶}) ∧ ^◡(1^st ↾ (V × {𝐶})) Fn V))
49	48	simprd 498	. . . . . . 7 ⊢ (𝐶 ∈ 𝐵 → ^◡(1^st ↾ (V × {𝐶})) Fn V)
50		vex 3496	. . . . . . 7 ⊢ 𝑥 ∈ V
51		fvco2 6751	. . . . . . 7 ⊢ ((^◡(1^st ↾ (V × {𝐶})) Fn V ∧ 𝑥 ∈ V) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
52	49, 50, 51	sylancl 588	. . . . . 6 ⊢ (𝐶 ∈ 𝐵 → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
53	52	ad2antlr 725	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘ ^◡(1^st ↾ (V × {𝐶})))‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
54	46, 53	syl5eq 2866	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)))
55	2	adantr 483	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V)
56	50	a1i 11	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ V)
57		snidg 4591	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ {𝐶})
58	57	adantr 483	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ {𝐶})
59	56, 58	opelxpd 5586	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶}))
60	55, 59	jca 514	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶})):(V × {𝐶})–1-1-onto→V ∧ ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶})))
61	50	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐵 → 𝑥 ∈ V)
62	61, 57	opelxpd 5586	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐵 → ⟨𝑥, 𝐶⟩ ∈ (V × {𝐶}))
63	62	fvresd 6683	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐵 → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
64	63	adantr 483	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = (1^st ‘⟨𝑥, 𝐶⟩))
65		op1stg 7693	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
66	65	ancoms 461	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (1^st ‘⟨𝑥, 𝐶⟩) = 𝑥)
67	64, 66	eqtrd 2854	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ((1^st ↾ (V × {𝐶}))‘⟨𝑥, 𝐶⟩) = 𝑥)
68		f1ocnvfv 7027	. . . . . . . 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 6667	. . . . . 6 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
71	70	adantll 712	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝐹‘⟨𝑥, 𝐶⟩))
72		df-ov 7151	. . . . 5 ⊢ (𝑥𝐹𝐶) = (𝐹‘⟨𝑥, 𝐶⟩)
73	71, 72	syl6eqr 2872	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(^◡(1^st ↾ (V × {𝐶}))‘𝑥)) = (𝑥𝐹𝐶))
74	54, 73	eqtrd 2854	. . 3 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝑥𝐹𝐶))
75	74	mpteq2dva 5152	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))
76	45, 75	eqtrd 2854	1 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 = wceq 1531 ∈ wcel 2108 Vcvv 3493 ∩ cin 3933 ⊆ wss 3934 {csn 4559 ⟨cop 4565 ↦ cmpt 5137 × cxp 5546 ^◡ccnv 5547 dom cdm 5548 ran crn 5549 ↾ cres 5550 “ cima 5551 ∘ ccom 5552 Fun wfun 6342 Fn wfn 6343 –onto→wfo 6346 –1-1-onto→wf1o 6347 ‘cfv 6348 (class class class)co 7148 1^st c1st 7679

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7453

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ne 3015 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-sbc 3771 df-csb 3882 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-ov 7151 df-1st 7681 df-2nd 7682

This theorem is referenced by: curry2f 7795 curry2val 7796

W3C validator