Metamath Proof Explorer

Definition df-func

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)

Ref Expression
Assertion 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 ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfunc 
 |-  Func
1 vt 
 |-  t
2 ccat 
 |-  Cat
3 vu 
 |-  u
4 vf 
 |-  f
5 vg 
 |-  g
6 cbs 
 |-  Base
7 1 cv 
 |-  t
8 7 6 cfv 
 |-  ( Base ` t )
9 vb 
 |-  b
10 4 cv 
 |-  f
11 9 cv 
 |-  b
12 3 cv 
 |-  u
13 12 6 cfv 
 |-  ( Base ` u )
14 11 13 10 wf 
 |-  f : b --> ( Base ` u )
15 5 cv 
 |-  g
16 vz 
 |-  z
17 11 11 cxp 
 |-  ( b X. b )
18 c1st 
 |-  1st
19 16 cv 
 |-  z
20 19 18 cfv 
 |-  ( 1st ` z )
21 20 10 cfv 
 |-  ( f ` ( 1st ` z ) )
22 chom 
 |-  Hom
23 12 22 cfv 
 |-  ( Hom ` u )
24 c2nd 
 |-  2nd
25 19 24 cfv 
 |-  ( 2nd ` z )
26 25 10 cfv 
 |-  ( f ` ( 2nd ` z ) )
27 21 26 23 co 
 |-  ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) )
28 cmap 
 |-  ^m
29 7 22 cfv 
 |-  ( Hom ` t )
30 19 29 cfv 
 |-  ( ( Hom ` t ) ` z )
31 27 30 28 co 
 |-  ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) )
32 16 17 31 cixp 
 |-  X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) )
33 15 32 wcel 
 |-  g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) )
34 vx 
 |-  x
35 34 cv 
 |-  x
36 35 35 15 co 
 |-  ( x g x )
37 ccid 
 |-  Id
38 7 37 cfv 
 |-  ( Id ` t )
39 35 38 cfv 
 |-  ( ( Id ` t ) ` x )
40 39 36 cfv 
 |-  ( ( x g x ) ` ( ( Id ` t ) ` x ) )
41 12 37 cfv 
 |-  ( Id ` u )
42 35 10 cfv 
 |-  ( f ` x )
43 42 41 cfv 
 |-  ( ( Id ` u ) ` ( f ` x ) )
44 40 43 wceq 
 |-  ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) )
45 vy 
 |-  y
46 vm 
 |-  m
47 45 cv 
 |-  y
48 35 47 29 co 
 |-  ( x ( Hom ` t ) y )
49 vn 
 |-  n
50 47 19 29 co 
 |-  ( y ( Hom ` t ) z )
51 35 19 15 co 
 |-  ( x g z )
52 49 cv 
 |-  n
53 35 47 cop 
 |-  <. x , y >.
54 cco 
 |-  comp
55 7 54 cfv 
 |-  ( comp ` t )
56 53 19 55 co 
 |-  ( <. x , y >. ( comp ` t ) z )
57 46 cv 
 |-  m
58 52 57 56 co 
 |-  ( n ( <. x , y >. ( comp ` t ) z ) m )
59 58 51 cfv 
 |-  ( ( x g z ) ` ( n ( <. x , y >. ( comp ` t ) z ) m ) )
60 47 19 15 co 
 |-  ( y g z )
61 52 60 cfv 
 |-  ( ( y g z ) ` n )
62 47 10 cfv 
 |-  ( f ` y )
63 42 62 cop 
 |-  <. ( f ` x ) , ( f ` y ) >.
64 12 54 cfv 
 |-  ( comp ` u )
65 19 10 cfv 
 |-  ( f ` z )
66 63 65 64 co 
 |-  ( <. ( f ` x ) , ( f ` y ) >. ( comp ` u ) ( f ` z ) )
67 35 47 15 co 
 |-  ( x g y )
68 57 67 cfv 
 |-  ( ( x g y ) ` m )
69 61 68 66 co 
 |-  ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. ( comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) )
70 59 69 wceq 
 |-  ( ( 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 70 49 50 wral 
 |-  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 ) )
72 71 46 48 wral 
 |-  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 16 11 wral 
 |-  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 45 11 wral 
 |-  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 
 |-  ( ( ( 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 11 wral 
 |-  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 14 33 76 w3a 
 |-  ( 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 77 9 8 wsbc 
 |-  [. ( 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 ) ) ) )
79 78 4 5 copab 
 |-  { <. 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 ) ) ) ) }
80 1 3 2 2 79 cmpo 
 |-  ( 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 ) ) ) ) } )
81 0 80 wceq 
 |-  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 ) ) ) ) } )