Definition df-curf 17722

Description: Define the curry functor, which maps a functor 𝐹:𝐶 × 𝐷⟶𝐸 to curry_F (𝐹):𝐶⟶(𝐷⟶𝐸). (Contributed by Mario Carneiro, 11-Jan-2017.)

Assertion

Ref	Expression
df-curf	⊢ curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd ‘𝑒) / 𝑑⦌⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩)

Distinct variable group:   𝑐,𝑑,𝑓,𝑔,𝑥,𝑦,𝑒,𝑧

Detailed syntax breakdown of Definition df-curf

Step	Hyp	Ref	Expression
1		ccurf 17718	. 2 class curryF
2		ve	. . 3 setvar 𝑒
3		vf	. . 3 setvar 𝑓
4		cvv 3408	. . 3 class V
5		vc	. . . 4 setvar 𝑐
6	2	cv 1542	. . . . 5 class 𝑒
7		c1st 7759	. . . . 5 class 1st
8	6, 7	cfv 6380	. . . 4 class (1st ‘𝑒)
9		vd	. . . . 5 setvar 𝑑
10		c2nd 7760	. . . . . 6 class 2nd
11	6, 10	cfv 6380	. . . . 5 class (2nd ‘𝑒)
12		vx	. . . . . . 7 setvar 𝑥
13	5	cv 1542	. . . . . . . 8 class 𝑐
14		cbs 16760	. . . . . . . 8 class Base
15	13, 14	cfv 6380	. . . . . . 7 class (Base‘𝑐)
16		vy	. . . . . . . . 9 setvar 𝑦
17	9	cv 1542	. . . . . . . . . 10 class 𝑑
18	17, 14	cfv 6380	. . . . . . . . 9 class (Base‘𝑑)
19	12	cv 1542	. . . . . . . . . 10 class 𝑥
20	16	cv 1542	. . . . . . . . . 10 class 𝑦
21	3	cv 1542	. . . . . . . . . . 11 class 𝑓
22	21, 7	cfv 6380	. . . . . . . . . 10 class (1st ‘𝑓)
23	19, 20, 22	co 7213	. . . . . . . . 9 class (𝑥(1st ‘𝑓)𝑦)
24	16, 18, 23	cmpt 5135	. . . . . . . 8 class (𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦))
25		vz	. . . . . . . . 9 setvar 𝑧
26		vg	. . . . . . . . . 10 setvar 𝑔
27	25	cv 1542	. . . . . . . . . . 11 class 𝑧
28		chom 16813	. . . . . . . . . . . 12 class Hom
29	17, 28	cfv 6380	. . . . . . . . . . 11 class (Hom ‘𝑑)
30	20, 27, 29	co 7213	. . . . . . . . . 10 class (𝑦(Hom ‘𝑑)𝑧)
31		ccid 17168	. . . . . . . . . . . . 13 class Id
32	13, 31	cfv 6380	. . . . . . . . . . . 12 class (Id‘𝑐)
33	19, 32	cfv 6380	. . . . . . . . . . 11 class ((Id‘𝑐)‘𝑥)
34	26	cv 1542	. . . . . . . . . . 11 class 𝑔
35	19, 20	cop 4547	. . . . . . . . . . . 12 class ⟨𝑥, 𝑦⟩
36	19, 27	cop 4547	. . . . . . . . . . . 12 class ⟨𝑥, 𝑧⟩
37	21, 10	cfv 6380	. . . . . . . . . . . 12 class (2nd ‘𝑓)
38	35, 36, 37	co 7213	. . . . . . . . . . 11 class (⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)
39	33, 34, 38	co 7213	. . . . . . . . . 10 class (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)
40	26, 30, 39	cmpt 5135	. . . . . . . . 9 class (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔))
41	16, 25, 18, 18, 40	cmpo 7215	. . . . . . . 8 class (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))
42	24, 41	cop 4547	. . . . . . 7 class ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩
43	12, 15, 42	cmpt 5135	. . . . . 6 class (𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩)
44	13, 28	cfv 6380	. . . . . . . . 9 class (Hom ‘𝑐)
45	19, 20, 44	co 7213	. . . . . . . 8 class (𝑥(Hom ‘𝑐)𝑦)
46	17, 31	cfv 6380	. . . . . . . . . . 11 class (Id‘𝑑)
47	27, 46	cfv 6380	. . . . . . . . . 10 class ((Id‘𝑑)‘𝑧)
48	20, 27	cop 4547	. . . . . . . . . . 11 class ⟨𝑦, 𝑧⟩
49	36, 48, 37	co 7213	. . . . . . . . . 10 class (⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)
50	34, 47, 49	co 7213	. . . . . . . . 9 class (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧))
51	25, 18, 50	cmpt 5135	. . . . . . . 8 class (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))
52	26, 45, 51	cmpt 5135	. . . . . . 7 class (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧))))
53	12, 16, 15, 15, 52	cmpo 7215	. . . . . 6 class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))
54	43, 53	cop 4547	. . . . 5 class ⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩
55	9, 11, 54	csb 3811	. . . 4 class ⦋(2nd ‘𝑒) / 𝑑⦌⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩
56	5, 8, 55	csb 3811	. . 3 class ⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd ‘𝑒) / 𝑑⦌⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩
57	2, 3, 4, 4, 56	cmpo 7215	. 2 class (𝑒 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd ‘𝑒) / 𝑑⦌⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩)
58	1, 57	wceq 1543	1 wff curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑒) / 𝑐⦌⦋(2nd ‘𝑒) / 𝑑⦌⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st ‘𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd ‘𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩)

This definition is referenced by:  curfval  17731