Theorem curry1 7420

Description: Composition with ^◡(2^nd ↾ ({𝐶} × V)) turns any binary operation 𝐹 with a constant first operand into a function 𝐺 of the second operand only. This transformation is called "currying." (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Dec-2014.)

Hypothesis

Ref	Expression
curry1.1	⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))

Assertion

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

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

Proof of Theorem curry1

Step	Hyp	Ref	Expression
1		fnfun 6128	. . . . 5 ⊢ (𝐹 Fn (𝐴 × 𝐵) → Fun 𝐹)
2		2ndconst 7417	. . . . . 6 ⊢ (𝐶 ∈ 𝐴 → (2nd ↾ ({𝐶} × V)):({𝐶} × V)–1-1-onto→V)
3		dff1o3 6284	. . . . . . 7 ⊢ ((2nd ↾ ({𝐶} × V)):({𝐶} × V)–1-1-onto→V ↔ ((2nd ↾ ({𝐶} × V)):({𝐶} × V)–onto→V ∧ Fun ◡(2nd ↾ ({𝐶} × V))))
4	3	simprbi 484	. . . . . 6 ⊢ ((2nd ↾ ({𝐶} × V)):({𝐶} × V)–1-1-onto→V → Fun ◡(2nd ↾ ({𝐶} × V)))
5	2, 4	syl 17	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → Fun ◡(2nd ↾ ({𝐶} × V)))
6		funco 6071	. . . . 5 ⊢ ((Fun 𝐹 ∧ Fun ◡(2nd ↾ ({𝐶} × V))) → Fun (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))))
7	1, 5, 6	syl2an 583	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → Fun (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))))
8		dmco 5787	. . . . 5 ⊢ dom (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) = (◡◡(2nd ↾ ({𝐶} × V)) “ dom 𝐹)
9		fndm 6130	. . . . . . . 8 ⊢ (𝐹 Fn (𝐴 × 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
10	9	adantr 466	. . . . . . 7 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → dom 𝐹 = (𝐴 × 𝐵))
11	10	imaeq2d 5607	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → (◡◡(2nd ↾ ({𝐶} × V)) “ dom 𝐹) = (◡◡(2nd ↾ ({𝐶} × V)) “ (𝐴 × 𝐵)))
12		imacnvcnv 5740	. . . . . . . . 9 ⊢ (◡◡(2nd ↾ ({𝐶} × V)) “ (𝐴 × 𝐵)) = ((2nd ↾ ({𝐶} × V)) “ (𝐴 × 𝐵))
13		df-ima 5262	. . . . . . . . 9 ⊢ ((2nd ↾ ({𝐶} × V)) “ (𝐴 × 𝐵)) = ran ((2nd ↾ ({𝐶} × V)) ↾ (𝐴 × 𝐵))
14		resres 5550	. . . . . . . . . 10 ⊢ ((2nd ↾ ({𝐶} × V)) ↾ (𝐴 × 𝐵)) = (2nd ↾ (({𝐶} × V) ∩ (𝐴 × 𝐵)))
15	14	rneqi 5490	. . . . . . . . 9 ⊢ ran ((2nd ↾ ({𝐶} × V)) ↾ (𝐴 × 𝐵)) = ran (2nd ↾ (({𝐶} × V) ∩ (𝐴 × 𝐵)))
16	12, 13, 15	3eqtri 2797	. . . . . . . 8 ⊢ (◡◡(2nd ↾ ({𝐶} × V)) “ (𝐴 × 𝐵)) = ran (2nd ↾ (({𝐶} × V) ∩ (𝐴 × 𝐵)))
17		inxp 5393	. . . . . . . . . . . . 13 ⊢ (({𝐶} × V) ∩ (𝐴 × 𝐵)) = (({𝐶} ∩ 𝐴) × (V ∩ 𝐵))
18		incom 3956	. . . . . . . . . . . . . . 15 ⊢ (V ∩ 𝐵) = (𝐵 ∩ V)
19		inv1 4114	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∩ V) = 𝐵
20	18, 19	eqtri 2793	. . . . . . . . . . . . . 14 ⊢ (V ∩ 𝐵) = 𝐵
21	20	xpeq2i 5276	. . . . . . . . . . . . 13 ⊢ (({𝐶} ∩ 𝐴) × (V ∩ 𝐵)) = (({𝐶} ∩ 𝐴) × 𝐵)
22	17, 21	eqtri 2793	. . . . . . . . . . . 12 ⊢ (({𝐶} × V) ∩ (𝐴 × 𝐵)) = (({𝐶} ∩ 𝐴) × 𝐵)
23		snssi 4474	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐴 → {𝐶} ⊆ 𝐴)
24		df-ss 3737	. . . . . . . . . . . . . 14 ⊢ ({𝐶} ⊆ 𝐴 ↔ ({𝐶} ∩ 𝐴) = {𝐶})
25	23, 24	sylib 208	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐴 → ({𝐶} ∩ 𝐴) = {𝐶})
26	25	xpeq1d 5278	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐴 → (({𝐶} ∩ 𝐴) × 𝐵) = ({𝐶} × 𝐵))
27	22, 26	syl5eq 2817	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐴 → (({𝐶} × V) ∩ (𝐴 × 𝐵)) = ({𝐶} × 𝐵))
28	27	reseq2d 5534	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → (2nd ↾ (({𝐶} × V) ∩ (𝐴 × 𝐵))) = (2nd ↾ ({𝐶} × 𝐵)))
29	28	rneqd 5491	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → ran (2nd ↾ (({𝐶} × V) ∩ (𝐴 × 𝐵))) = ran (2nd ↾ ({𝐶} × 𝐵)))
30		2ndconst 7417	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → (2nd ↾ ({𝐶} × 𝐵)):({𝐶} × 𝐵)–1-1-onto→𝐵)
31		f1ofo 6285	. . . . . . . . . 10 ⊢ ((2nd ↾ ({𝐶} × 𝐵)):({𝐶} × 𝐵)–1-1-onto→𝐵 → (2nd ↾ ({𝐶} × 𝐵)):({𝐶} × 𝐵)–onto→𝐵)
32		forn 6259	. . . . . . . . . 10 ⊢ ((2nd ↾ ({𝐶} × 𝐵)):({𝐶} × 𝐵)–onto→𝐵 → ran (2nd ↾ ({𝐶} × 𝐵)) = 𝐵)
33	30, 31, 32	3syl 18	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → ran (2nd ↾ ({𝐶} × 𝐵)) = 𝐵)
34	29, 33	eqtrd 2805	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → ran (2nd ↾ (({𝐶} × V) ∩ (𝐴 × 𝐵))) = 𝐵)
35	16, 34	syl5eq 2817	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → (◡◡(2nd ↾ ({𝐶} × V)) “ (𝐴 × 𝐵)) = 𝐵)
36	35	adantl 467	. . . . . 6 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → (◡◡(2nd ↾ ({𝐶} × V)) “ (𝐴 × 𝐵)) = 𝐵)
37	11, 36	eqtrd 2805	. . . . 5 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → (◡◡(2nd ↾ ({𝐶} × V)) “ dom 𝐹) = 𝐵)
38	8, 37	syl5eq 2817	. . . 4 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → dom (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) = 𝐵)
39		curry1.1	. . . . . 6 ⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))
40	39	fneq1i 6125	. . . . 5 ⊢ (𝐺 Fn 𝐵 ↔ (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) Fn 𝐵)
41		df-fn 6034	. . . . 5 ⊢ ((𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) Fn 𝐵 ↔ (Fun (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ∧ dom (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) = 𝐵))
42	40, 41	bitri 264	. . . 4 ⊢ (𝐺 Fn 𝐵 ↔ (Fun (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ∧ dom (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) = 𝐵))
43	7, 38, 42	sylanbrc 572	. . 3 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐺 Fn 𝐵)
44		dffn5 6383	. . 3 ⊢ (𝐺 Fn 𝐵 ↔ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐺‘𝑥)))
45	43, 44	sylib 208	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐺‘𝑥)))
46	39	fveq1i 6333	. . . . 5 ⊢ (𝐺‘𝑥) = ((𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))‘𝑥)
47		dff1o4 6286	. . . . . . . . 9 ⊢ ((2nd ↾ ({𝐶} × V)):({𝐶} × V)–1-1-onto→V ↔ ((2nd ↾ ({𝐶} × V)) Fn ({𝐶} × V) ∧ ◡(2nd ↾ ({𝐶} × V)) Fn V))
48	2, 47	sylib 208	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → ((2nd ↾ ({𝐶} × V)) Fn ({𝐶} × V) ∧ ◡(2nd ↾ ({𝐶} × V)) Fn V))
49	48	simprd 483	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → ◡(2nd ↾ ({𝐶} × V)) Fn V)
50		vex 3354	. . . . . . . 8 ⊢ 𝑥 ∈ V
51		fvco2 6415	. . . . . . . 8 ⊢ ((◡(2nd ↾ ({𝐶} × V)) Fn V ∧ 𝑥 ∈ V) → ((𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))‘𝑥) = (𝐹‘(◡(2nd ↾ ({𝐶} × V))‘𝑥)))
52	50, 51	mpan2 671	. . . . . . 7 ⊢ (◡(2nd ↾ ({𝐶} × V)) Fn V → ((𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))‘𝑥) = (𝐹‘(◡(2nd ↾ ({𝐶} × V))‘𝑥)))
53	49, 52	syl 17	. . . . . 6 ⊢ (𝐶 ∈ 𝐴 → ((𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))‘𝑥) = (𝐹‘(◡(2nd ↾ ({𝐶} × V))‘𝑥)))
54	53	ad2antlr 706	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))‘𝑥) = (𝐹‘(◡(2nd ↾ ({𝐶} × V))‘𝑥)))
55	46, 54	syl5eq 2817	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = (𝐹‘(◡(2nd ↾ ({𝐶} × V))‘𝑥)))
56	2	adantr 466	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (2nd ↾ ({𝐶} × V)):({𝐶} × V)–1-1-onto→V)
57		snidg 4345	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ {𝐶})
58	57, 50	jctir 510	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝐴 → (𝐶 ∈ {𝐶} ∧ 𝑥 ∈ V))
59		opelxp 5286	. . . . . . . . . . 11 ⊢ (⟨𝐶, 𝑥⟩ ∈ ({𝐶} × V) ↔ (𝐶 ∈ {𝐶} ∧ 𝑥 ∈ V))
60	58, 59	sylibr 224	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → ⟨𝐶, 𝑥⟩ ∈ ({𝐶} × V))
61	60	adantr 466	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ⟨𝐶, 𝑥⟩ ∈ ({𝐶} × V))
62	56, 61	jca 501	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ((2nd ↾ ({𝐶} × V)):({𝐶} × V)–1-1-onto→V ∧ ⟨𝐶, 𝑥⟩ ∈ ({𝐶} × V)))
63		fvres 6348	. . . . . . . . . . 11 ⊢ (⟨𝐶, 𝑥⟩ ∈ ({𝐶} × V) → ((2nd ↾ ({𝐶} × V))‘⟨𝐶, 𝑥⟩) = (2nd ‘⟨𝐶, 𝑥⟩))
64	60, 63	syl 17	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → ((2nd ↾ ({𝐶} × V))‘⟨𝐶, 𝑥⟩) = (2nd ‘⟨𝐶, 𝑥⟩))
65		op2ndg 7328	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑥 ∈ V) → (2nd ‘⟨𝐶, 𝑥⟩) = 𝑥)
66	50, 65	mpan2 671	. . . . . . . . . 10 ⊢ (𝐶 ∈ 𝐴 → (2nd ‘⟨𝐶, 𝑥⟩) = 𝑥)
67	64, 66	eqtrd 2805	. . . . . . . . 9 ⊢ (𝐶 ∈ 𝐴 → ((2nd ↾ ({𝐶} × V))‘⟨𝐶, 𝑥⟩) = 𝑥)
68	67	adantr 466	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ((2nd ↾ ({𝐶} × V))‘⟨𝐶, 𝑥⟩) = 𝑥)
69		f1ocnvfv 6677	. . . . . . . 8 ⊢ (((2nd ↾ ({𝐶} × V)):({𝐶} × V)–1-1-onto→V ∧ ⟨𝐶, 𝑥⟩ ∈ ({𝐶} × V)) → (((2nd ↾ ({𝐶} × V))‘⟨𝐶, 𝑥⟩) = 𝑥 → (◡(2nd ↾ ({𝐶} × V))‘𝑥) = ⟨𝐶, 𝑥⟩))
70	62, 68, 69	sylc 65	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (◡(2nd ↾ ({𝐶} × V))‘𝑥) = ⟨𝐶, 𝑥⟩)
71	70	fveq2d 6336	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝐹‘(◡(2nd ↾ ({𝐶} × V))‘𝑥)) = (𝐹‘⟨𝐶, 𝑥⟩))
72	71	adantll 693	. . . . 5 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝐹‘(◡(2nd ↾ ({𝐶} × V))‘𝑥)) = (𝐹‘⟨𝐶, 𝑥⟩))
73		df-ov 6796	. . . . 5 ⊢ (𝐶𝐹𝑥) = (𝐹‘⟨𝐶, 𝑥⟩)
74	72, 73	syl6eqr 2823	. . . 4 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝐹‘(◡(2nd ↾ ({𝐶} × V))‘𝑥)) = (𝐶𝐹𝑥))
75	55, 74	eqtrd 2805	. . 3 ⊢ (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = (𝐶𝐹𝑥))
76	75	mpteq2dva 4878	. 2 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥)))
77	45, 76	eqtrd 2805	1 ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥)))

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145  Vcvv 3351   ∩ cin 3722   ⊆ wss 3723  {csn 4316  ⟨cop 4322   ↦ cmpt 4863   × cxp 5247  ^◡ccnv 5248  dom cdm 5249  ran crn 5250   ↾ cres 5251   “ cima 5252   ∘ ccom 5253  Fun wfun 6025   Fn wfn 6026  –onto→wfo 6029  –1-1-onto→wf1o 6030  ‘cfv 6031  (class class class)co 6793  2^nd c2nd 7314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-1st 7315  df-2nd 7316

This theorem is referenced by:  curry1val  7421  curry1f  7422