Metamath Proof Explorer

Definition df-catc

Description: Definition of the category Cat, which consists of all categories in the universe u (i.e. " u -small categories", see definition 3.44. of Adamek p. 39), with functors as the morphisms. Definition 3.47 of Adamek p. 40. We do not introduce a specific definition for " u -large categories", which can be expressed as ( Cat \ u ) . (Contributed by Mario Carneiro, 3-Jan-2017)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccatc 
 |-  CatCat
1 vu 
 |-  u
2 cvv 
 |-  _V
3 1 cv 
 |-  u
4 ccat 
 |-  Cat
5 3 4 cin 
 |-  ( u i^i Cat )
6 vb 
 |-  b
7 cbs 
 |-  Base
8 cnx 
 |-  ndx
9 8 7 cfv 
 |-  ( Base ` ndx )
10 6 cv 
 |-  b
11 9 10 cop 
 |-  <. ( Base ` ndx ) , b >.
12 chom 
 |-  Hom
13 8 12 cfv 
 |-  ( Hom ` ndx )
14 vx 
 |-  x
15 vy 
 |-  y
16 14 cv 
 |-  x
17 cfunc 
 |-  Func
18 15 cv 
 |-  y
19 16 18 17 co 
 |-  ( x Func y )
20 14 15 10 10 19 cmpo 
 |-  ( x e. b , y e. b |-> ( x Func y ) )
21 13 20 cop 
 |-  <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >.
22 cco 
 |-  comp
23 8 22 cfv 
 |-  ( comp ` ndx )
24 vv 
 |-  v
25 10 10 cxp 
 |-  ( b X. b )
26 vz 
 |-  z
27 vg 
 |-  g
28 c2nd 
 |-  2nd
29 24 cv 
 |-  v
30 29 28 cfv 
 |-  ( 2nd ` v )
31 26 cv 
 |-  z
32 30 31 17 co 
 |-  ( ( 2nd ` v ) Func z )
33 vf 
 |-  f
34 29 17 cfv 
 |-  ( Func ` v )
35 27 cv 
 |-  g
36 ccofu 
 |-  o.func
37 33 cv 
 |-  f
38 35 37 36 co 
 |-  ( g o.func f )
39 27 33 32 34 38 cmpo 
 |-  ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) )
40 24 26 25 10 39 cmpo 
 |-  ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) )
41 23 40 cop 
 |-  <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >.
42 11 21 41 ctp 
 |-  { <. ( 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 ) ) ) >. }
43 6 5 42 csb 
 |-  [_ ( 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 ) ) ) >. }
44 1 2 43 cmpt 
 |-  ( 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 ) ) ) >. } )
45 0 44 wceq 
 |-  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 ) ) ) >. } )