Metamath Proof Explorer

Definition df-cat

Description: A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated with those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. Definition in Lang p. 53. In contrast to definition 3.1 of Adamek p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" ( ( Basec ) ), the morphisms "hom" ( ( Homc ) ) and the composition law "o" ( ( compc ) ). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in Adamek p. 21 and df-cid . (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-cat 
|- Cat = { c | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. ( comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccat 
 |-  Cat
1 vc 
 |-  c
2 cbs 
 |-  Base
3 1 cv 
 |-  c
4 3 2 cfv 
 |-  ( Base ` c )
5 vb 
 |-  b
6 chom 
 |-  Hom
7 3 6 cfv 
 |-  ( Hom ` c )
8 vh 
 |-  h
9 cco 
 |-  comp
10 3 9 cfv 
 |-  ( comp ` c )
11 vo 
 |-  o
12 vx 
 |-  x
13 5 cv 
 |-  b
14 vg 
 |-  g
15 12 cv 
 |-  x
16 8 cv 
 |-  h
17 15 15 16 co 
 |-  ( x h x )
18 vy 
 |-  y
19 vf 
 |-  f
20 18 cv 
 |-  y
21 20 15 16 co 
 |-  ( y h x )
22 14 cv 
 |-  g
23 20 15 cop 
 |-  <. y , x >.
24 11 cv 
 |-  o
25 23 15 24 co 
 |-  ( <. y , x >. o x )
26 19 cv 
 |-  f
27 22 26 25 co 
 |-  ( g ( <. y , x >. o x ) f )
28 27 26 wceq 
 |-  ( g ( <. y , x >. o x ) f ) = f
29 28 19 21 wral 
 |-  A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f
30 15 20 16 co 
 |-  ( x h y )
31 15 15 cop 
 |-  <. x , x >.
32 31 20 24 co 
 |-  ( <. x , x >. o y )
33 26 22 32 co 
 |-  ( f ( <. x , x >. o y ) g )
34 33 26 wceq 
 |-  ( f ( <. x , x >. o y ) g ) = f
35 34 19 30 wral 
 |-  A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f
36 29 35 wa 
 |-  ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
37 36 18 13 wral 
 |-  A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
38 37 14 17 wrex 
 |-  E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
39 vz 
 |-  z
40 39 cv 
 |-  z
41 20 40 16 co 
 |-  ( y h z )
42 15 20 cop 
 |-  <. x , y >.
43 42 40 24 co 
 |-  ( <. x , y >. o z )
44 22 26 43 co 
 |-  ( g ( <. x , y >. o z ) f )
45 15 40 16 co 
 |-  ( x h z )
46 44 45 wcel 
 |-  ( g ( <. x , y >. o z ) f ) e. ( x h z )
47 vw 
 |-  w
48 vk 
 |-  k
49 47 cv 
 |-  w
50 40 49 16 co 
 |-  ( z h w )
51 48 cv 
 |-  k
52 20 40 cop 
 |-  <. y , z >.
53 52 49 24 co 
 |-  ( <. y , z >. o w )
54 51 22 53 co 
 |-  ( k ( <. y , z >. o w ) g )
55 42 49 24 co 
 |-  ( <. x , y >. o w )
56 54 26 55 co 
 |-  ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f )
57 15 40 cop 
 |-  <. x , z >.
58 57 49 24 co 
 |-  ( <. x , z >. o w )
59 51 44 58 co 
 |-  ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) )
60 56 59 wceq 
 |-  ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) )
61 60 48 50 wral 
 |-  A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) )
62 61 47 13 wral 
 |-  A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) )
63 46 62 wa 
 |-  ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
64 63 14 41 wral 
 |-  A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
65 64 19 30 wral 
 |-  A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
66 65 39 13 wral 
 |-  A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
67 66 18 13 wral 
 |-  A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
68 38 67 wa 
 |-  ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
69 68 12 13 wral 
 |-  A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
70 69 11 10 wsbc 
 |-  [. ( comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
71 70 8 7 wsbc 
 |-  [. ( Hom ` c ) / h ]. [. ( comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
72 71 5 4 wsbc 
 |-  [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. ( comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
73 72 1 cab 
 |-  { c | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. ( comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) }
74 0 73 wceq 
 |-  Cat = { c | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. ( comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) }