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

Definition df-catc 13943
Description: Definition of the category Cat, which consists of all categories in the universe  u, with functors as the morphisms. (Contributed by Mario Carneiro, 3-Jan-2017.)
Assertion
Ref Expression
df-catc  |- CatCat  =  ( u  e.  _V  |->  [_ ( u  i^i  Cat )  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. (  Hom  `  ndx ) ,  ( x  e.  b ,  y  e.  b  |->  ( x  Func  y ) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( b  X.  b ) ,  z  e.  b  |->  ( g  e.  ( ( 2nd `  v ) 
Func  z ) ,  f  e.  (  Func  `  v )  |->  ( g  o.func  f ) ) )
>. } )
Distinct variable group:    f, b, g, u, v, x, y, z

Detailed syntax breakdown of Definition df-catc
StepHypRef Expression
1 ccatc 13942 . 2  class CatCat
2 vu . . 3  set  u
3 cvv 2801 . . 3  class  _V
4 vb . . . 4  set  b
52cv 1631 . . . . 5  class  u
6 ccat 13582 . . . . 5  class  Cat
75, 6cin 3164 . . . 4  class  ( u  i^i  Cat )
8 cnx 13161 . . . . . . 7  class  ndx
9 cbs 13164 . . . . . . 7  class  Base
108, 9cfv 5271 . . . . . 6  class  ( Base `  ndx )
114cv 1631 . . . . . 6  class  b
1210, 11cop 3656 . . . . 5  class  <. ( Base `  ndx ) ,  b >.
13 chom 13235 . . . . . . 7  class  Hom
148, 13cfv 5271 . . . . . 6  class  (  Hom  `  ndx )
15 vx . . . . . . 7  set  x
16 vy . . . . . . 7  set  y
1715cv 1631 . . . . . . . 8  class  x
1816cv 1631 . . . . . . . 8  class  y
19 cfunc 13744 . . . . . . . 8  class  Func
2017, 18, 19co 5874 . . . . . . 7  class  ( x 
Func  y )
2115, 16, 11, 11, 20cmpt2 5876 . . . . . 6  class  ( x  e.  b ,  y  e.  b  |->  ( x 
Func  y ) )
2214, 21cop 3656 . . . . 5  class  <. (  Hom  `  ndx ) ,  ( x  e.  b ,  y  e.  b 
|->  ( x  Func  y
) ) >.
23 cco 13236 . . . . . . 7  class comp
248, 23cfv 5271 . . . . . 6  class  (comp `  ndx )
25 vv . . . . . . 7  set  v
26 vz . . . . . . 7  set  z
2711, 11cxp 4703 . . . . . . 7  class  ( b  X.  b )
28 vg . . . . . . . 8  set  g
29 vf . . . . . . . 8  set  f
3025cv 1631 . . . . . . . . . 10  class  v
31 c2nd 6137 . . . . . . . . . 10  class  2nd
3230, 31cfv 5271 . . . . . . . . 9  class  ( 2nd `  v )
3326cv 1631 . . . . . . . . 9  class  z
3432, 33, 19co 5874 . . . . . . . 8  class  ( ( 2nd `  v ) 
Func  z )
3530, 19cfv 5271 . . . . . . . 8  class  (  Func  `  v )
3628cv 1631 . . . . . . . . 9  class  g
3729cv 1631 . . . . . . . . 9  class  f
38 ccofu 13746 . . . . . . . . 9  class  o.func
3936, 37, 38co 5874 . . . . . . . 8  class  ( g  o.func  f )
4028, 29, 34, 35, 39cmpt2 5876 . . . . . . 7  class  ( g  e.  ( ( 2nd `  v )  Func  z
) ,  f  e.  (  Func  `  v ) 
|->  ( g  o.func  f )
)
4125, 26, 27, 11, 40cmpt2 5876 . . . . . 6  class  ( v  e.  ( b  X.  b ) ,  z  e.  b  |->  ( g  e.  ( ( 2nd `  v )  Func  z
) ,  f  e.  (  Func  `  v ) 
|->  ( g  o.func  f )
) )
4224, 41cop 3656 . . . . 5  class  <. (comp ` 
ndx ) ,  ( v  e.  ( b  X.  b ) ,  z  e.  b  |->  ( g  e.  ( ( 2nd `  v ) 
Func  z ) ,  f  e.  (  Func  `  v )  |->  ( g  o.func  f ) ) )
>.
4312, 22, 42ctp 3655 . . . 4  class  { <. (
Base `  ndx ) ,  b >. ,  <. (  Hom  `  ndx ) ,  ( x  e.  b ,  y  e.  b 
|->  ( x  Func  y
) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( b  X.  b ) ,  z  e.  b  |->  ( g  e.  ( ( 2nd `  v ) 
Func  z ) ,  f  e.  (  Func  `  v )  |->  ( g  o.func  f ) ) )
>. }
444, 7, 43csb 3094 . . 3  class  [_ (
u  i^i  Cat )  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. (  Hom  `  ndx ) ,  ( x  e.  b ,  y  e.  b  |->  ( x  Func  y ) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( b  X.  b ) ,  z  e.  b  |->  ( g  e.  ( ( 2nd `  v ) 
Func  z ) ,  f  e.  (  Func  `  v )  |->  ( g  o.func  f ) ) )
>. }
452, 3, 44cmpt 4093 . 2  class  ( u  e.  _V  |->  [_ (
u  i^i  Cat )  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. (  Hom  `  ndx ) ,  ( x  e.  b ,  y  e.  b  |->  ( x  Func  y ) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( b  X.  b ) ,  z  e.  b  |->  ( g  e.  ( ( 2nd `  v ) 
Func  z ) ,  f  e.  (  Func  `  v )  |->  ( g  o.func  f ) ) )
>. } )
461, 45wceq 1632 1  wff CatCat  =  ( u  e.  _V  |->  [_ ( u  i^i  Cat )  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. (  Hom  `  ndx ) ,  ( x  e.  b ,  y  e.  b  |->  ( x  Func  y ) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( b  X.  b ) ,  z  e.  b  |->  ( g  e.  ( ( 2nd `  v ) 
Func  z ) ,  f  e.  (  Func  `  v )  |->  ( g  o.func  f ) ) )
>. } )
Colors of variables: wff set class
This definition is referenced by:  catcval  13944
  Copyright terms: Public domain W3C validator