df-fuc - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-fuc		Structured version Visualization version GIF version

Definition df-fuc 18122

Description: Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)

**Assertion**
Ref	Expression
df-fuc	⊢ FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩})

Distinct variable group: 𝑎,𝑏,𝑓,𝑔,ℎ,𝑡,𝑢,𝑣,𝑥

**Detailed syntax breakdown of Definition df-fuc**
Step	Hyp	Ref	Expression
1		cfuc 18120	. 2 class FuncCat
2		vt	. . 3 setvar 𝑡
3		vu	. . 3 setvar 𝑢
4		ccat 17838	. . 3 class Cat
5		cnx 17371	. . . . . 6 class ndx
6		cbs 17387	. . . . . 6 class Base
7	5, 6	cfv 6538	. . . . 5 class (Base‘ndx)
8	2	cv 1569	. . . . . 6 class 𝑡
9	3	cv 1569	. . . . . 6 class 𝑢
10		cfunc 18029	. . . . . 6 class Func
11	8, 9, 10	co 7420	. . . . 5 class (𝑡 Func 𝑢)
12	7, 11	cop 4590	. . . 4 class ⟨(Base‘ndx), (𝑡 Func 𝑢)⟩
13		chom 17439	. . . . . 6 class Hom
14	5, 13	cfv 6538	. . . . 5 class (Hom ‘ndx)
15		cnat 18119	. . . . . 6 class Nat
16	8, 9, 15	co 7420	. . . . 5 class (𝑡 Nat 𝑢)
17	14, 16	cop 4590	. . . 4 class ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩
18		cco 17440	. . . . . 6 class comp
19	5, 18	cfv 6538	. . . . 5 class (comp‘ndx)
20		vv	. . . . . 6 setvar 𝑣
21		vh	. . . . . 6 setvar ℎ
22	11, 11	cxp 5649	. . . . . 6 class ((𝑡 Func 𝑢) × (𝑡 Func 𝑢))
23		vf	. . . . . . 7 setvar 𝑓
24	20	cv 1569	. . . . . . . 8 class 𝑣
25		c1st 7999	. . . . . . . 8 class 1^st
26	24, 25	cfv 6538	. . . . . . 7 class (1^st ‘𝑣)
27		vg	. . . . . . . 8 setvar 𝑔
28		c2nd 8000	. . . . . . . . 9 class 2^nd
29	24, 28	cfv 6538	. . . . . . . 8 class (2^nd ‘𝑣)
30		vb	. . . . . . . . 9 setvar 𝑏
31		va	. . . . . . . . 9 setvar 𝑎
32	27	cv 1569	. . . . . . . . . 10 class 𝑔
33	21	cv 1569	. . . . . . . . . 10 class ℎ
34	32, 33, 16	co 7420	. . . . . . . . 9 class (𝑔(𝑡 Nat 𝑢)ℎ)
35	23	cv 1569	. . . . . . . . . 10 class 𝑓
36	35, 32, 16	co 7420	. . . . . . . . 9 class (𝑓(𝑡 Nat 𝑢)𝑔)
37		vx	. . . . . . . . . 10 setvar 𝑥
38	8, 6	cfv 6538	. . . . . . . . . 10 class (Base‘𝑡)
39	37	cv 1569	. . . . . . . . . . . 12 class 𝑥
40	30	cv 1569	. . . . . . . . . . . 12 class 𝑏
41	39, 40	cfv 6538	. . . . . . . . . . 11 class (𝑏‘𝑥)
42	31	cv 1569	. . . . . . . . . . . 12 class 𝑎
43	39, 42	cfv 6538	. . . . . . . . . . 11 class (𝑎‘𝑥)
44	35, 25	cfv 6538	. . . . . . . . . . . . . 14 class (1^st ‘𝑓)
45	39, 44	cfv 6538	. . . . . . . . . . . . 13 class ((1^st ‘𝑓)‘𝑥)
46	32, 25	cfv 6538	. . . . . . . . . . . . . 14 class (1^st ‘𝑔)
47	39, 46	cfv 6538	. . . . . . . . . . . . 13 class ((1^st ‘𝑔)‘𝑥)
48	45, 47	cop 4590	. . . . . . . . . . . 12 class ⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩
49	33, 25	cfv 6538	. . . . . . . . . . . . 13 class (1^st ‘ℎ)
50	39, 49	cfv 6538	. . . . . . . . . . . 12 class ((1^st ‘ℎ)‘𝑥)
51	9, 18	cfv 6538	. . . . . . . . . . . 12 class (comp‘𝑢)
52	48, 50, 51	co 7420	. . . . . . . . . . 11 class (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))
53	41, 43, 52	co 7420	. . . . . . . . . 10 class ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))
54	37, 38, 53	cmpt 5186	. . . . . . . . 9 class (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))
55	30, 31, 34, 36, 54	cmpo 7422	. . . . . . . 8 class (𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))
56	27, 29, 55	csb 3847	. . . . . . 7 class ⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))
57	23, 26, 56	csb 3847	. . . . . 6 class ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))
58	20, 21, 22, 11, 57	cmpo 7422	. . . . 5 class (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))
59	19, 58	cop 4590	. . . 4 class ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩
60	12, 17, 59	ctp 4588	. . 3 class {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩}
61	2, 3, 4, 4, 60	cmpo 7422	. 2 class (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩})
62	1, 61	wceq 1570	1 wff FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑢)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩})

Colors of variables: wff setvar class

This definition is used by: fnfuc 18123 fucval 18136

W3C validator