Definition df-func 10724

Description: Function returning all the functors from a category t to a category u. Intuitively a functor associate any morphism of t to a morphism of u, any object of t to an object of u, and respects the identity and the composition. It is a way to say that the structures of t and u are "equivalent". Here to capture the idea that a functor associate any object of t to an object of u we write that it associate any identity of t to an identity of u which simplifies the definition.

Assertion

Ref

Expression

df-func

|- Func = {<.<.t, u>., v>. | ((t e. Cat /\ u e. Cat) /\ v = {f | (f:dom (dom` t)-->dom (dom` u) /\ (A.o e. dom (id` t)E.p e. dom (id` u)(f` ((id` t)` o)) = ((id` u)` p) /\ (A.m e. dom (dom` t)(f` ((id` t)` ((dom` t)` m))) = ((id` u)` ((dom` u)` (f` m))) /\ A.m e. dom (dom` t)(f` ((id` t)` ((cod` t)` m))) = ((id` u)` ((cod` u)` (f` m)))) /\ A.m e. dom (dom` t)A.n e. dom (dom` t)(((cod` t)` n) = ((dom` t)` m) -> (f` (m(o` t)n)) = ((f` m)(o` u)(f` n)))))})}

Distinct variable group:   u,t,v,f,o,p,m,n

Detailed syntax breakdown of Definition df-func

Step	Hyp	Ref	Expression
1		cfunc 10722	. 2 class Func
2		vt	. . . . . . 7 set t
3	2	cv 957	. . . . . 6 class t
4		ccat 10656	. . . . . 6 class Cat
5	3, 4	wcel 960	. . . . 5 wff t e. Cat
6		vu	. . . . . . 7 set u
7	6	cv 957	. . . . . 6 class u
8	7, 4	wcel 960	. . . . 5 wff u e. Cat
9	5, 8	wa 223	. . . 4 wff (t e. Cat /\ u e. Cat)
10		vv	. . . . . 6 set v
11	10	cv 957	. . . . 5 class v
12		cdom_ 10615	. . . . . . . . . 10 class dom
13	3, 12	cfv 3188	. . . . . . . . 9 class (dom` t)
14	13	cdm 3176	. . . . . . . 8 class dom (dom` t)
15	7, 12	cfv 3188	. . . . . . . . 9 class (dom` u)
16	15	cdm 3176	. . . . . . . 8 class dom (dom` u)
17		vf	. . . . . . . . 9 set f
18	17	cv 957	. . . . . . . 8 class f
19	14, 16, 18	wf 3184	. . . . . . 7 wff f:dom (dom` t)-->dom (dom` u)
20		vo	. . . . . . . . . . . . . 14 set o
21	20	cv 957	. . . . . . . . . . . . 13 class o
22		cid_ 10617	. . . . . . . . . . . . . 14 class id
23	3, 22	cfv 3188	. . . . . . . . . . . . 13 class (id` t)
24	21, 23	cfv 3188	. . . . . . . . . . . 12 class ((id` t)` o)
25	24, 18	cfv 3188	. . . . . . . . . . 11 class (f` ((id` t)` o))
26		vp	. . . . . . . . . . . . 13 set p
27	26	cv 957	. . . . . . . . . . . 12 class p
28	7, 22	cfv 3188	. . . . . . . . . . . 12 class (id` u)
29	27, 28	cfv 3188	. . . . . . . . . . 11 class ((id` u)` p)
30	25, 29	wceq 958	. . . . . . . . . 10 wff (f` ((id` t)` o)) = ((id` u)` p)
31	28	cdm 3176	. . . . . . . . . 10 class dom (id` u)
32	30, 26, 31	wrex 1649	. . . . . . . . 9 wff E.p e. dom (id` u)(f` ((id` t)` o)) = ((id` u)` p)
33	23	cdm 3176	. . . . . . . . 9 class dom (id` t)
34	32, 20, 33	wral 1648	. . . . . . . 8 wff A.o e. dom (id` t)E.p e. dom (id` u)(f` ((id` t)` o)) = ((id` u)` p)
35		vm	. . . . . . . . . . . . . . 15 set m
36	35	cv 957	. . . . . . . . . . . . . 14 class m
37	36, 13	cfv 3188	. . . . . . . . . . . . 13 class ((dom` t)` m)
38	37, 23	cfv 3188	. . . . . . . . . . . 12 class ((id` t)` ((dom` t)` m))
39	38, 18	cfv 3188	. . . . . . . . . . 11 class (f` ((id` t)` ((dom` t)` m)))
40	36, 18	cfv 3188	. . . . . . . . . . . . 13 class (f` m)
41	40, 15	cfv 3188	. . . . . . . . . . . 12 class ((dom` u)` (f` m))
42	41, 28	cfv 3188	. . . . . . . . . . 11 class ((id` u)` ((dom` u)` (f` m)))
43	39, 42	wceq 958	. . . . . . . . . 10 wff (f` ((id` t)` ((dom` t)` m))) = ((id` u)` ((dom` u)` (f` m)))
44	43, 35, 14	wral 1648	. . . . . . . . 9 wff A.m e. dom (dom` t)(f` ((id` t)` ((dom` t)` m))) = ((id` u)` ((dom` u)` (f` m)))
45		ccod_ 10616	. . . . . . . . . . . . . . 15 class cod
46	3, 45	cfv 3188	. . . . . . . . . . . . . 14 class (cod` t)
47	36, 46	cfv 3188	. . . . . . . . . . . . 13 class ((cod` t)` m)
48	47, 23	cfv 3188	. . . . . . . . . . . 12 class ((id` t)` ((cod` t)` m))
49	48, 18	cfv 3188	. . . . . . . . . . 11 class (f` ((id` t)` ((cod` t)` m)))
50	7, 45	cfv 3188	. . . . . . . . . . . . 13 class (cod` u)
51	40, 50	cfv 3188	. . . . . . . . . . . 12 class ((cod` u)` (f` m))
52	51, 28	cfv 3188	. . . . . . . . . . 11 class ((id` u)` ((cod` u)` (f` m)))
53	49, 52	wceq 958	. . . . . . . . . 10 wff (f` ((id` t)` ((cod` t)` m))) = ((id` u)` ((cod` u)` (f` m)))
54	53, 35, 14	wral 1648	. . . . . . . . 9 wff A.m e. dom (dom` t)(f` ((id` t)` ((cod` t)` m))) = ((id` u)` ((cod` u)` (f` m)))
55	44, 54	wa 223	. . . . . . . 8 wff (A.m e. dom (dom` t)(f` ((id` t)` ((dom` t)` m))) = ((id` u)` ((dom` u)` (f` m))) /\ A.m e. dom (dom` t)(f` ((id` t)` ((cod` t)` m))) = ((id` u)` ((cod` u)` (f` m))))
56		vn	. . . . . . . . . . . . . 14 set n
57	56	cv 957	. . . . . . . . . . . . 13 class n
58	57, 46	cfv 3188	. . . . . . . . . . . 12 class ((cod` t)` n)
59	58, 37	wceq 958	. . . . . . . . . . 11 wff ((cod` t)` n) = ((dom` t)` m)
60		co_ 10618	. . . . . . . . . . . . . . 15 class o
61	3, 60	cfv 3188	. . . . . . . . . . . . . 14 class (o` t)
62	36, 57, 61	co 3969	. . . . . . . . . . . . 13 class (m(o` t)n)
63	62, 18	cfv 3188	. . . . . . . . . . . 12 class (f` (m(o` t)n))
64	57, 18	cfv 3188	. . . . . . . . . . . . 13 class (f` n)
65	7, 60	cfv 3188	. . . . . . . . . . . . 13 class (o` u)
66	40, 64, 65	co 3969	. . . . . . . . . . . 12 class ((f` m)(o` u)(f` n))
67	63, 66	wceq 958	. . . . . . . . . . 11 wff (f` (m(o` t)n)) = ((f` m)(o` u)(f` n))
68	59, 67	wi 3	. . . . . . . . . 10 wff (((cod` t)` n) = ((dom` t)` m) -> (f` (m(o` t)n)) = ((f` m)(o` u)(f` n)))
69	68, 56, 14	wral 1648	. . . . . . . . 9 wff A.n e. dom (dom` t)(((cod` t)` n) = ((dom` t)` m) -> (f` (m(o` t)n)) = ((f` m)(o` u)(f` n)))
70	69, 35, 14	wral 1648	. . . . . . . 8 wff A.m e. dom (dom` t)A.n e. dom (dom` t)(((cod` t)` n) = ((dom` t)` m) -> (f` (m(o` t)n)) = ((f` m)(o` u)(f` n)))
71	34, 55, 70	w3a 777	. . . . . . 7 wff (A.o e. dom (id` t)E.p e. dom (id` u)(f` ((id` t)` o)) = ((id` u)` p) /\ (A.m e. dom (dom` t)(f` ((id` t)` ((dom` t)` m))) = ((id` u)` ((dom` u)` (f` m))) /\ A.m e. dom (dom` t)(f` ((id` t)` ((cod` t)` m))) = ((id` u)` ((cod` u)` (f` m)))) /\ A.m e. dom (dom` t)A.n e. dom (dom` t)(((cod` t)` n) = ((dom` t)` m) -> (f` (m(o` t)n)) = ((f` m)(o` u)(f` n))))
72	19, 71	wa 223	. . . . . 6 wff (f:dom (dom` t)-->dom (dom` u) /\ (A.o e. dom (id` t)E.p e. dom (id` u)(f` ((id` t)` o)) = ((id` u)` p) /\ (A.m e. dom (dom` t)(f` ((id` t)` ((dom` t)` m))) = ((id` u)` ((dom` u)` (f` m))) /\ A.m e. dom (dom` t)(f` ((id` t)` ((cod` t)` m))) = ((id` u)` ((cod` u)` (f` m)))) /\ A.m e. dom (dom` t)A.n e. dom (dom` t)(((cod` t)` n) = ((dom` t)` m) -> (f` (m(o` t)n)) = ((f` m)(o` u)(f` n)))))
73	72, 17	cab 1466	. . . . 5 class {f | (f:dom (dom` t)-->dom (dom` u) /\ (A.o e. dom (id` t)E.p e. dom (id` u)(f` ((id` t)` o)) = ((id` u)` p) /\ (A.m e. dom (dom` t)(f` ((id` t)` ((dom` t)` m))) = ((id` u)` ((dom` u)` (f` m))) /\ A.m e. dom (dom` t)(f` ((id` t)` ((cod` t)` m))) = ((id` u)` ((cod` u)` (f` m)))) /\ A.m e. dom (dom` t)A.n e. dom (dom` t)(((cod` t)` n) = ((dom` t)` m) -> (f` (m(o` t)n)) = ((f` m)(o` u)(f` n)))))}
74	11, 73	wceq 958	. . . 4 wff v = {f | (f:dom (dom` t)-->dom (dom` u) /\ (A.o