Definition df-func 16518

Description: Function returning all the functors from a category t to a category u. Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). Intuitively a functor associates any morphism of t to a morphism of u, any object of t to an object of u, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of t to an object of u we write it associates any identity of t to an identity of u 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 = ( t e. Cat , u e. Cat |-> { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) } )

Distinct variable group:   f, b, g, m, n, t, u, x, y, z

Detailed syntax breakdown of Definition df-func

Step	Hyp	Ref	Expression
1		cfunc 16514	. 2 class Func
2		vt	. . 3 setvar t
3		vu	. . 3 setvar u
4		ccat 16325	. . 3 class Cat
5		vb	. . . . . . . 8 setvar b
6	5	cv 1482	. . . . . . 7 class b
7	3	cv 1482	. . . . . . . 8 class u
8		cbs 15857	. . . . . . . 8 class Base
9	7, 8	cfv 5888	. . . . . . 7 class ( Base ` u )
10		vf	. . . . . . . 8 setvar f
11	10	cv 1482	. . . . . . 7 class f
12	6, 9, 11	wf 5884	. . . . . 6 wff f : b --> ( Base ` u )
13		vg	. . . . . . . 8 setvar g
14	13	cv 1482	. . . . . . 7 class g
15		vz	. . . . . . . 8 setvar z
16	6, 6	cxp 5112	. . . . . . . 8 class ( b X. b )
17	15	cv 1482	. . . . . . . . . . . 12 class z
18		c1st 7166	. . . . . . . . . . . 12 class 1st
19	17, 18	cfv 5888	. . . . . . . . . . 11 class ( 1st ` z )
20	19, 11	cfv 5888	. . . . . . . . . 10 class ( f ` ( 1st ` z ) )
21		c2nd 7167	. . . . . . . . . . . 12 class 2nd
22	17, 21	cfv 5888	. . . . . . . . . . 11 class ( 2nd ` z )
23	22, 11	cfv 5888	. . . . . . . . . 10 class ( f ` ( 2nd ` z ) )
24		chom 15952	. . . . . . . . . . 11 class Hom
25	7, 24	cfv 5888	. . . . . . . . . 10 class ( Hom ` u )
26	20, 23, 25	co 6650	. . . . . . . . 9 class ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) )
27	2	cv 1482	. . . . . . . . . . 11 class t
28	27, 24	cfv 5888	. . . . . . . . . 10 class ( Hom ` t )
29	17, 28	cfv 5888	. . . . . . . . 9 class ( ( Hom ` t ) ` z )
30		cmap 7857	. . . . . . . . 9 class ^m
31	26, 29, 30	co 6650	. . . . . . . 8 class ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) )
32	15, 16, 31	cixp 7908	. . . . . . 7 class X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) )
33	14, 32	wcel 1990	. . . . . 6 wff g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) )
34		vx	. . . . . . . . . . . 12 setvar x
35	34	cv 1482	. . . . . . . . . . 11 class x
36		ccid 16326	. . . . . . . . . . . 12 class Id
37	27, 36	cfv 5888	. . . . . . . . . . 11 class ( Id ` t )
38	35, 37	cfv 5888	. . . . . . . . . 10 class ( ( Id ` t ) ` x )
39	35, 35, 14	co 6650	. . . . . . . . . 10 class ( x g x )
40	38, 39	cfv 5888	. . . . . . . . 9 class ( ( x g x ) ` ( ( Id ` t ) ` x ) )
41	35, 11	cfv 5888	. . . . . . . . . 10 class ( f ` x )
42	7, 36	cfv 5888	. . . . . . . . . 10 class ( Id ` u )
43	41, 42	cfv 5888	. . . . . . . . 9 class ( ( Id ` u ) ` ( f ` x ) )
44	40, 43	wceq 1483	. . . . . . . 8 wff ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) )
45		vn	. . . . . . . . . . . . . . . 16 setvar n
46	45	cv 1482	. . . . . . . . . . . . . . 15 class n
47		vm	. . . . . . . . . . . . . . . 16 setvar m
48	47	cv 1482	. . . . . . . . . . . . . . 15 class m
49		vy	. . . . . . . . . . . . . . . . . 18 setvar y
50	49	cv 1482	. . . . . . . . . . . . . . . . 17 class y
51	35, 50	cop 4183	. . . . . . . . . . . . . . . 16 class <. x , y >.
52		cco 15953	. . . . . . . . . . . . . . . . 17 class comp
53	27, 52	cfv 5888	. . . . . . . . . . . . . . . 16 class (comp ` t )
54	51, 17, 53	co 6650	. . . . . . . . . . . . . . 15 class ( <. x , y >. (comp ` t ) z )
55	46, 48, 54	co 6650	. . . . . . . . . . . . . 14 class ( n ( <. x , y >. (comp ` t ) z ) m )
56	35, 17, 14	co 6650	. . . . . . . . . . . . . 14 class ( x g z )
57	55, 56	cfv 5888	. . . . . . . . . . . . 13 class ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) )
58	50, 17, 14	co 6650	. . . . . . . . . . . . . . 15 class ( y g z )
59	46, 58	cfv 5888	. . . . . . . . . . . . . 14 class ( ( y g z ) ` n )
60	35, 50, 14	co 6650	. . . . . . . . . . . . . . 15 class ( x g y )
61	48, 60	cfv 5888	. . . . . . . . . . . . . 14 class ( ( x g y ) ` m )
62	50, 11	cfv 5888	. . . . . . . . . . . . . . . 16 class ( f ` y )
63	41, 62	cop 4183	. . . . . . . . . . . . . . 15 class <. ( f ` x ) , ( f ` y ) >.
64	17, 11	cfv 5888	. . . . . . . . . . . . . . 15 class ( f ` z )
65	7, 52	cfv 5888	. . . . . . . . . . . . . . 15 class (comp ` u )
66	63, 64, 65	co 6650	. . . . . . . . . . . . . 14 class ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) )
67	59, 61, 66	co 6650	. . . . . . . . . . . . 13 class ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) )
68	57, 67	wceq 1483	. . . . . . . . . . . 12 wff ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) )
69	50, 17, 28	co 6650	. . . . . . . . . . . 12 class ( y ( Hom ` t ) z )
70	68, 45, 69	wral 2912	. . . . . . . . . . 11 wff A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) )
71	35, 50, 28	co 6650	. . . . . . . . . . 11 class ( x ( Hom ` t ) y )
72	70, 47, 71	wral 2912	. . . . . . . . . 10 wff A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) )
73	72, 15, 6	wral 2912	. . . . . . . . 9 wff A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) )
74	73, 49, 6	wral 2912	. . . . . . . 8 wff A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) )
75	44, 74	wa 384	. . . . . . 7 wff ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) )
76	75, 34, 6	wral 2912	. . . . . 6 wff A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) )
77	12, 33, 76	w3a 1037	. . . . 5 wff ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) )
78	27, 8	cfv 5888	. . . . 5 class ( Base ` t )
79	77, 5, 78	wsbc 3435	. . . 4 wff [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) )
80	79, 10, 13	copab 4712	. . 3 class { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) }
81	2, 3, 4, 4, 80	cmpt2 6652	. 2 class ( t e. Cat , u e. Cat |-> { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) } )
82	1, 81	wceq 1483	1 wff Func = ( t e. Cat , u e. Cat |-> { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) } )

This definition is referenced by:  relfunc  16522  funcrcl  16523  isfunc  16524