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, without the axiom CAT 1, i.e., pairwise disjointness of hom-sets ( cat1 ). See setc2obas and setc2ohom for a counterexample. 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 ) ) ) ) }