MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-func Unicode version

Definition df-func 13732
Description: Function returning all the functors from a category  t to a category  u. 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. (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
StepHypRef Expression
1 cfunc 13728 . 2  class  Func
2 vt . . 3  set  t
3 vu . . 3  set  u
4 ccat 13566 . . 3  class  Cat
5 vb . . . . . . . 8  set  b
65cv 1622 . . . . . . 7  class  b
73cv 1622 . . . . . . . 8  class  u
8 cbs 13148 . . . . . . . 8  class  Base
97, 8cfv 5255 . . . . . . 7  class  ( Base `  u )
10 vf . . . . . . . 8  set  f
1110cv 1622 . . . . . . 7  class  f
126, 9, 11wf 5251 . . . . . 6  wff  f : b --> ( Base `  u
)
13 vg . . . . . . . 8  set  g
1413cv 1622 . . . . . . 7  class  g
15 vz . . . . . . . 8  set  z
166, 6cxp 4687 . . . . . . . 8  class  ( b  X.  b )
1715cv 1622 . . . . . . . . . . . 12  class  z
18 c1st 6120 . . . . . . . . . . . 12  class  1st
1917, 18cfv 5255 . . . . . . . . . . 11  class  ( 1st `  z )
2019, 11cfv 5255 . . . . . . . . . 10  class  ( f `
 ( 1st `  z
) )
21 c2nd 6121 . . . . . . . . . . . 12  class  2nd
2217, 21cfv 5255 . . . . . . . . . . 11  class  ( 2nd `  z )
2322, 11cfv 5255 . . . . . . . . . 10  class  ( f `
 ( 2nd `  z
) )
24 chom 13219 . . . . . . . . . . 11  class  Hom
257, 24cfv 5255 . . . . . . . . . 10  class  (  Hom  `  u )
2620, 23, 25co 5858 . . . . . . . . 9  class  ( ( f `  ( 1st `  z ) ) (  Hom  `  u )
( f `  ( 2nd `  z ) ) )
272cv 1622 . . . . . . . . . . 11  class  t
2827, 24cfv 5255 . . . . . . . . . 10  class  (  Hom  `  t )
2917, 28cfv 5255 . . . . . . . . 9  class  ( (  Hom  `  t ) `  z )
30 cmap 6772 . . . . . . . . 9  class  ^m
3126, 29, 30co 5858 . . . . . . . 8  class  ( ( ( f `  ( 1st `  z ) ) (  Hom  `  u
) ( f `  ( 2nd `  z ) ) )  ^m  (
(  Hom  `  t ) `
 z ) )
3215, 16, 31cixp 6817 . . . . . . 7  class  X_ z  e.  ( b  X.  b
) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  u )
( f `  ( 2nd `  z ) ) )  ^m  ( (  Hom  `  t ) `  z ) )
3314, 32wcel 1684 . . . . . 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  set  x
3534cv 1622 . . . . . . . . . . 11  class  x
36 ccid 13567 . . . . . . . . . . . 12  class  Id
3727, 36cfv 5255 . . . . . . . . . . 11  class  ( Id
`  t )
3835, 37cfv 5255 . . . . . . . . . 10  class  ( ( Id `  t ) `
 x )
3935, 35, 14co 5858 . . . . . . . . . 10  class  ( x g x )
4038, 39cfv 5255 . . . . . . . . 9  class  ( ( x g x ) `
 ( ( Id
`  t ) `  x ) )
4135, 11cfv 5255 . . . . . . . . . 10  class  ( f `
 x )
427, 36cfv 5255 . . . . . . . . . 10  class  ( Id
`  u )
4341, 42cfv 5255 . . . . . . . . 9  class  ( ( Id `  u ) `
 ( f `  x ) )
4440, 43wceq 1623 . . . . . . . 8  wff  ( ( x g x ) `
 ( ( Id
`  t ) `  x ) )  =  ( ( Id `  u ) `  (
f `  x )
)
45 vn . . . . . . . . . . . . . . . 16  set  n
4645cv 1622 . . . . . . . . . . . . . . 15  class  n
47 vm . . . . . . . . . . . . . . . 16  set  m
4847cv 1622 . . . . . . . . . . . . . . 15  class  m
49 vy . . . . . . . . . . . . . . . . . 18  set  y
5049cv 1622 . . . . . . . . . . . . . . . . 17  class  y
5135, 50cop 3643 . . . . . . . . . . . . . . . 16  class  <. x ,  y >.
52 cco 13220 . . . . . . . . . . . . . . . . 17  class comp
5327, 52cfv 5255 . . . . . . . . . . . . . . . 16  class  (comp `  t )
5451, 17, 53co 5858 . . . . . . . . . . . . . . 15  class  ( <.
x ,  y >.
(comp `  t )
z )
5546, 48, 54co 5858 . . . . . . . . . . . . . 14  class  ( n ( <. x ,  y
>. (comp `  t )
z ) m )
5635, 17, 14co 5858 . . . . . . . . . . . . . 14  class  ( x g z )
5755, 56cfv 5255 . . . . . . . . . . . . 13  class  ( ( x g z ) `
 ( n (
<. x ,  y >.
(comp `  t )
z ) m ) )
5850, 17, 14co 5858 . . . . . . . . . . . . . . 15  class  ( y g z )
5946, 58cfv 5255 . . . . . . . . . . . . . 14  class  ( ( y g z ) `
 n )
6035, 50, 14co 5858 . . . . . . . . . . . . . . 15  class  ( x g y )
6148, 60cfv 5255 . . . . . . . . . . . . . 14  class  ( ( x g y ) `
 m )
6250, 11cfv 5255 . . . . . . . . . . . . . . . 16  class  ( f `
 y )
6341, 62cop 3643 . . . . . . . . . . . . . . 15  class  <. (
f `  x ) ,  ( f `  y ) >.
6417, 11cfv 5255 . . . . . . . . . . . . . . 15  class  ( f `
 z )
657, 52cfv 5255 . . . . . . . . . . . . . . 15  class  (comp `  u )
6663, 64, 65co 5858 . . . . . . . . . . . . . 14  class  ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  u )
( f `  z
) )
6759, 61, 66co 5858 . . . . . . . . . . . . 13  class  ( ( ( y g z ) `  n ) ( <. ( f `  x ) ,  ( f `  y )
>. (comp `  u )
( f `  z
) ) ( ( x g y ) `
 m ) )
6857, 67wceq 1623 . . . . . . . . . . . 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 ) )
6950, 17, 28co 5858 . . . . . . . . . . . 12  class  ( y (  Hom  `  t
) z )
7068, 45, 69wral 2543 . . . . . . . . . . 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 ) )
7135, 50, 28co 5858 . . . . . . . . . . 11  class  ( x (  Hom  `  t
) y )
7270, 47, 71wral 2543 . . . . . . . . . 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 ) )
7372, 15, 6wral 2543 . . . . . . . . 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 ) )
7473, 49, 6wral 2543 . . . . . . . 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 ) )
7544, 74wa 358 . . . . . . 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 ) ) )
7675, 34, 6wral 2543 . . . . . 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 ) ) )
7712, 33, 76w3a 934 . . . . 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 ) ) ) )
7827, 8cfv 5255 . . . . 5  class  ( Base `  t )
7977, 5, 78wsbc 2991 . . . 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 ) ) ) )
8079, 10, 13copab 4076 . . 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 ) ) ) ) }
812, 3, 4, 4, 80cmpt2 5860 . 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 ) ) ) ) } )
821, 81wceq 1623 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 ) ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  relfunc  13736  funcrcl  13737  isfunc  13738
  Copyright terms: Public domain W3C validator