Definition df-func 17573

Description: Function returning all the functors from a category 𝑡 to a category 𝑢. Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). Intuitively a functor associates any morphism of 𝑡 to a morphism of 𝑢, any object of 𝑡 to an object of 𝑢, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of 𝑡 to an object of 𝑢 we write it associates any identity of 𝑡 to an identity of 𝑢 which simplifies the definition. According to remark 3.19 in [Adamek] p. 30, "a functor F : A -> B is technically a family of functions; one from Ob(A) to Ob(B) [here: f, called "the object part" in the following], and for each pair (A,A') of A-objects, one from hom(A,A') to hom(FA, FA') [here: g, called "the morphism part" in the following]". (Contributed by FL, 10-Feb-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
df-func	⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})

Distinct variable group:   𝑓,𝑏,𝑔,𝑚,𝑛,𝑡,𝑢,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-func

Step	Hyp	Ref	Expression
1		cfunc 17569	. 2 class Func
2		vt	. . 3 setvar 𝑡
3		vu	. . 3 setvar 𝑢
4		ccat 17373	. . 3 class Cat
5		vb	. . . . . . . 8 setvar 𝑏
6	5	cv 1538	. . . . . . 7 class 𝑏
7	3	cv 1538	. . . . . . . 8 class 𝑢
8		cbs 16912	. . . . . . . 8 class Base
9	7, 8	cfv 6433	. . . . . . 7 class (Base‘𝑢)
10		vf	. . . . . . . 8 setvar 𝑓
11	10	cv 1538	. . . . . . 7 class 𝑓
12	6, 9, 11	wf 6429	. . . . . 6 wff 𝑓:𝑏⟶(Base‘𝑢)
13		vg	. . . . . . . 8 setvar 𝑔
14	13	cv 1538	. . . . . . 7 class 𝑔
15		vz	. . . . . . . 8 setvar 𝑧
16	6, 6	cxp 5587	. . . . . . . 8 class (𝑏 × 𝑏)
17	15	cv 1538	. . . . . . . . . . . 12 class 𝑧
18		c1st 7829	. . . . . . . . . . . 12 class 1st
19	17, 18	cfv 6433	. . . . . . . . . . 11 class (1st ‘𝑧)
20	19, 11	cfv 6433	. . . . . . . . . 10 class (𝑓‘(1st ‘𝑧))
21		c2nd 7830	. . . . . . . . . . . 12 class 2nd
22	17, 21	cfv 6433	. . . . . . . . . . 11 class (2nd ‘𝑧)
23	22, 11	cfv 6433	. . . . . . . . . 10 class (𝑓‘(2nd ‘𝑧))
24		chom 16973	. . . . . . . . . . 11 class Hom
25	7, 24	cfv 6433	. . . . . . . . . 10 class (Hom ‘𝑢)
26	20, 23, 25	co 7275	. . . . . . . . 9 class ((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧)))
27	2	cv 1538	. . . . . . . . . . 11 class 𝑡
28	27, 24	cfv 6433	. . . . . . . . . 10 class (Hom ‘𝑡)
29	17, 28	cfv 6433	. . . . . . . . 9 class ((Hom ‘𝑡)‘𝑧)
30		cmap 8615	. . . . . . . . 9 class ↑m
31	26, 29, 30	co 7275	. . . . . . . 8 class (((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧))
32	15, 16, 31	cixp 8685	. . . . . . 7 class X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧))
33	14, 32	wcel 2106	. . . . . 6 wff 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧))
34		vx	. . . . . . . . . . . 12 setvar 𝑥
35	34	cv 1538	. . . . . . . . . . 11 class 𝑥
36		ccid 17374	. . . . . . . . . . . 12 class Id
37	27, 36	cfv 6433	. . . . . . . . . . 11 class (Id‘𝑡)
38	35, 37	cfv 6433	. . . . . . . . . 10 class ((Id‘𝑡)‘𝑥)
39	35, 35, 14	co 7275	. . . . . . . . . 10 class (𝑥𝑔𝑥)
40	38, 39	cfv 6433	. . . . . . . . 9 class ((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥))
41	35, 11	cfv 6433	. . . . . . . . . 10 class (𝑓‘𝑥)
42	7, 36	cfv 6433	. . . . . . . . . 10 class (Id‘𝑢)
43	41, 42	cfv 6433	. . . . . . . . 9 class ((Id‘𝑢)‘(𝑓‘𝑥))
44	40, 43	wceq 1539	. . . . . . . 8 wff ((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥))
45		vn	. . . . . . . . . . . . . . . 16 setvar 𝑛
46	45	cv 1538	. . . . . . . . . . . . . . 15 class 𝑛
47		vm	. . . . . . . . . . . . . . . 16 setvar 𝑚
48	47	cv 1538	. . . . . . . . . . . . . . 15 class 𝑚
49		vy	. . . . . . . . . . . . . . . . . 18 setvar 𝑦
50	49	cv 1538	. . . . . . . . . . . . . . . . 17 class 𝑦
51	35, 50	cop 4567	. . . . . . . . . . . . . . . 16 class ⟨𝑥, 𝑦⟩
52		cco 16974	. . . . . . . . . . . . . . . . 17 class comp
53	27, 52	cfv 6433	. . . . . . . . . . . . . . . 16 class (comp‘𝑡)
54	51, 17, 53	co 7275	. . . . . . . . . . . . . . 15 class (⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)
55	46, 48, 54	co 7275	. . . . . . . . . . . . . 14 class (𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)
56	35, 17, 14	co 7275	. . . . . . . . . . . . . 14 class (𝑥𝑔𝑧)
57	55, 56	cfv 6433	. . . . . . . . . . . . 13 class ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚))
58	50, 17, 14	co 7275	. . . . . . . . . . . . . . 15 class (𝑦𝑔𝑧)
59	46, 58	cfv 6433	. . . . . . . . . . . . . 14 class ((𝑦𝑔𝑧)‘𝑛)
60	35, 50, 14	co 7275	. . . . . . . . . . . . . . 15 class (𝑥𝑔𝑦)
61	48, 60	cfv 6433	. . . . . . . . . . . . . 14 class ((𝑥𝑔𝑦)‘𝑚)
62	50, 11	cfv 6433	. . . . . . . . . . . . . . . 16 class (𝑓‘𝑦)
63	41, 62	cop 4567	. . . . . . . . . . . . . . 15 class ⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩
64	17, 11	cfv 6433	. . . . . . . . . . . . . . 15 class (𝑓‘𝑧)
65	7, 52	cfv 6433	. . . . . . . . . . . . . . 15 class (comp‘𝑢)
66	63, 64, 65	co 7275	. . . . . . . . . . . . . 14 class (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))
67	59, 61, 66	co 7275	. . . . . . . . . . . . 13 class (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))
68	57, 67	wceq 1539	. . . . . . . . . . . 12 wff ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))
69	50, 17, 28	co 7275	. . . . . . . . . . . 12 class (𝑦(Hom ‘𝑡)𝑧)
70	68, 45, 69	wral 3064	. . . . . . . . . . 11 wff ∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))
71	35, 50, 28	co 7275	. . . . . . . . . . 11 class (𝑥(Hom ‘𝑡)𝑦)
72	70, 47, 71	wral 3064	. . . . . . . . . 10 wff ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))
73	72, 15, 6	wral 3064	. . . . . . . . 9 wff ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))
74	73, 49, 6	wral 3064	. . . . . . . 8 wff ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))
75	44, 74	wa 396	. . . . . . 7 wff (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))
76	75, 34, 6	wral 3064	. . . . . 6 wff ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))
77	12, 33, 76	w3a 1086	. . . . 5 wff (𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
78	27, 8	cfv 6433	. . . . 5 class (Base‘𝑡)
79	77, 5, 78	wsbc 3716	. . . 4 wff [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
80	79, 10, 13	copab 5136	. . 3 class {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}
81	2, 3, 4, 4, 80	cmpo 7277	. 2 class (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
82	1, 81	wceq 1539	1 wff Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})

This definition is referenced by:  relfunc  17577  funcrcl  17578  isfunc  17579