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

Definition df-cat 15574
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" ( ( Base `  c
)), the morphisms "hom" ( ( Hom  `  c )) and the composition law "o" (
(comp `  c )). 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 15575. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
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 ) ) ) ) }
Distinct variable group:    b, c, f, g, h, k, o, w, x, y, z

Detailed syntax breakdown of Definition df-cat
StepHypRef Expression
1 ccat 15570 . 2  class  Cat
2 vg . . . . . . . . . . . . . . 15  setvar  g
32cv 1436 . . . . . . . . . . . . . 14  class  g
4 vf . . . . . . . . . . . . . . 15  setvar  f
54cv 1436 . . . . . . . . . . . . . 14  class  f
6 vy . . . . . . . . . . . . . . . . 17  setvar  y
76cv 1436 . . . . . . . . . . . . . . . 16  class  y
8 vx . . . . . . . . . . . . . . . . 17  setvar  x
98cv 1436 . . . . . . . . . . . . . . . 16  class  x
107, 9cop 4004 . . . . . . . . . . . . . . 15  class  <. y ,  x >.
11 vo . . . . . . . . . . . . . . . 16  setvar  o
1211cv 1436 . . . . . . . . . . . . . . 15  class  o
1310, 9, 12co 6306 . . . . . . . . . . . . . 14  class  ( <.
y ,  x >. o x )
143, 5, 13co 6306 . . . . . . . . . . . . 13  class  ( g ( <. y ,  x >. o x ) f )
1514, 5wceq 1437 . . . . . . . . . . . 12  wff  ( g ( <. y ,  x >. o x ) f )  =  f
16 vh . . . . . . . . . . . . . 14  setvar  h
1716cv 1436 . . . . . . . . . . . . 13  class  h
187, 9, 17co 6306 . . . . . . . . . . . 12  class  ( y h x )
1915, 4, 18wral 2771 . . . . . . . . . . 11  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
209, 9cop 4004 . . . . . . . . . . . . . . 15  class  <. x ,  x >.
2120, 7, 12co 6306 . . . . . . . . . . . . . 14  class  ( <.
x ,  x >. o y )
225, 3, 21co 6306 . . . . . . . . . . . . 13  class  ( f ( <. x ,  x >. o y ) g )
2322, 5wceq 1437 . . . . . . . . . . . 12  wff  ( f ( <. x ,  x >. o y ) g )  =  f
249, 7, 17co 6306 . . . . . . . . . . . 12  class  ( x h y )
2523, 4, 24wral 2771 . . . . . . . . . . 11  wff  A. f  e.  ( x h y ) ( f (
<. x ,  x >. o y ) g )  =  f
2619, 25wa 370 . . . . . . . . . 10  wff  ( 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 )
27 vb . . . . . . . . . . 11  setvar  b
2827cv 1436 . . . . . . . . . 10  class  b
2926, 6, 28wral 2771 . . . . . . . . 9  wff  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 )
309, 9, 17co 6306 . . . . . . . . 9  class  ( x h x )
3129, 2, 30wrex 2772 . . . . . . . 8  wff  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 )
329, 7cop 4004 . . . . . . . . . . . . . . . 16  class  <. x ,  y >.
33 vz . . . . . . . . . . . . . . . . 17  setvar  z
3433cv 1436 . . . . . . . . . . . . . . . 16  class  z
3532, 34, 12co 6306 . . . . . . . . . . . . . . 15  class  ( <.
x ,  y >.
o z )
363, 5, 35co 6306 . . . . . . . . . . . . . 14  class  ( g ( <. x ,  y
>. o z ) f )
379, 34, 17co 6306 . . . . . . . . . . . . . 14  class  ( x h z )
3836, 37wcel 1872 . . . . . . . . . . . . 13  wff  ( g ( <. x ,  y
>. o z ) f )  e.  ( x h z )
39 vk . . . . . . . . . . . . . . . . . . 19  setvar  k
4039cv 1436 . . . . . . . . . . . . . . . . . 18  class  k
417, 34cop 4004 . . . . . . . . . . . . . . . . . . 19  class  <. y ,  z >.
42 vw . . . . . . . . . . . . . . . . . . . 20  setvar  w
4342cv 1436 . . . . . . . . . . . . . . . . . . 19  class  w
4441, 43, 12co 6306 . . . . . . . . . . . . . . . . . 18  class  ( <.
y ,  z >.
o w )
4540, 3, 44co 6306 . . . . . . . . . . . . . . . . 17  class  ( k ( <. y ,  z
>. o w ) g )
4632, 43, 12co 6306 . . . . . . . . . . . . . . . . 17  class  ( <.
x ,  y >.
o w )
4745, 5, 46co 6306 . . . . . . . . . . . . . . . 16  class  ( ( k ( <. y ,  z >. o
w ) g ) ( <. x ,  y
>. o w ) f )
489, 34cop 4004 . . . . . . . . . . . . . . . . . 18  class  <. x ,  z >.
4948, 43, 12co 6306 . . . . . . . . . . . . . . . . 17  class  ( <.
x ,  z >.
o w )
5040, 36, 49co 6306 . . . . . . . . . . . . . . . 16  class  ( k ( <. x ,  z
>. o w ) ( g ( <. x ,  y >. o
z ) f ) )
5147, 50wceq 1437 . . . . . . . . . . . . . . 15  wff  ( ( k ( <. y ,  z >. o
w ) g ) ( <. x ,  y
>. o w ) f )  =  ( k ( <. x ,  z
>. o w ) ( g ( <. x ,  y >. o
z ) f ) )
5234, 43, 17co 6306 . . . . . . . . . . . . . . 15  class  ( z h w )
5351, 39, 52wral 2771 . . . . . . . . . . . . . 14  wff  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 ) )
5453, 42, 28wral 2771 . . . . . . . . . . . . 13  wff  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 ) )
5538, 54wa 370 . . . . . . . . . . . 12  wff  ( ( 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 ) ) )
567, 34, 17co 6306 . . . . . . . . . . . 12  class  ( y h z )
5755, 2, 56wral 2771 . . . . . . . . . . 11  wff  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 ) ) )
5857, 4, 24wral 2771 . . . . . . . . . 10  wff  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 ) ) )
5958, 33, 28wral 2771 . . . . . . . . 9  wff  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 ) ) )
6059, 6, 28wral 2771 . . . . . . . 8  wff  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 ) ) )
6131, 60wa 370 . . . . . . 7  wff  ( 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 ) ) ) )
6261, 8, 28wral 2771 . . . . . 6  wff  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 ) ) ) )
63 vc . . . . . . . 8  setvar  c
6463cv 1436 . . . . . . 7  class  c
65 cco 15202 . . . . . . 7  class comp
6664, 65cfv 5601 . . . . . 6  class  (comp `  c )
6762, 11, 66wsbc 3299 . . . . 5  wff  [. (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 ) ) ) )
68 chom 15201 . . . . . 6  class  Hom
6964, 68cfv 5601 . . . . 5  class  ( Hom  `  c )
7067, 16, 69wsbc 3299 . . . 4  wff  [. ( 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 ) ) ) )
71 cbs 15121 . . . . 5  class  Base
7264, 71cfv 5601 . . . 4  class  ( Base `  c )
7370, 27, 72wsbc 3299 . . 3  wff  [. ( 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 ) ) ) )
7473, 63cab 2407 . 2  class  { 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 ) ) ) ) }
751, 74wceq 1437 1  wff  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 ) ) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  iscat  15578
  Copyright terms: Public domain W3C validator