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

Definition df-cat 13813
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 to 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. (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 13809 . 2  class  Cat
2 vg . . . . . . . . . . . . . . 15  set  g
32cv 1648 . . . . . . . . . . . . . 14  class  g
4 vf . . . . . . . . . . . . . . 15  set  f
54cv 1648 . . . . . . . . . . . . . 14  class  f
6 vy . . . . . . . . . . . . . . . . 17  set  y
76cv 1648 . . . . . . . . . . . . . . . 16  class  y
8 vx . . . . . . . . . . . . . . . . 17  set  x
98cv 1648 . . . . . . . . . . . . . . . 16  class  x
107, 9cop 3753 . . . . . . . . . . . . . . 15  class  <. y ,  x >.
11 vo . . . . . . . . . . . . . . . 16  set  o
1211cv 1648 . . . . . . . . . . . . . . 15  class  o
1310, 9, 12co 6013 . . . . . . . . . . . . . 14  class  ( <.
y ,  x >. o x )
143, 5, 13co 6013 . . . . . . . . . . . . 13  class  ( g ( <. y ,  x >. o x ) f )
1514, 5wceq 1649 . . . . . . . . . . . 12  wff  ( g ( <. y ,  x >. o x ) f )  =  f
16 vh . . . . . . . . . . . . . 14  set  h
1716cv 1648 . . . . . . . . . . . . 13  class  h
187, 9, 17co 6013 . . . . . . . . . . . 12  class  ( y h x )
1915, 4, 18wral 2642 . . . . . . . . . . 11  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
209, 9cop 3753 . . . . . . . . . . . . . . 15  class  <. x ,  x >.
2120, 7, 12co 6013 . . . . . . . . . . . . . 14  class  ( <.
x ,  x >. o y )
225, 3, 21co 6013 . . . . . . . . . . . . 13  class  ( f ( <. x ,  x >. o y ) g )
2322, 5wceq 1649 . . . . . . . . . . . 12  wff  ( f ( <. x ,  x >. o y ) g )  =  f
249, 7, 17co 6013 . . . . . . . . . . . 12  class  ( x h y )
2523, 4, 24wral 2642 . . . . . . . . . . 11  wff  A. f  e.  ( x h y ) ( f (
<. x ,  x >. o y ) g )  =  f
2619, 25wa 359 . . . . . . . . . 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  set  b
2827cv 1648 . . . . . . . . . 10  class  b
2926, 6, 28wral 2642 . . . . . . . . 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 6013 . . . . . . . . 9  class  ( x h x )
3129, 2, 30wrex 2643 . . . . . . . 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 3753 . . . . . . . . . . . . . . . 16  class  <. x ,  y >.
33 vz . . . . . . . . . . . . . . . . 17  set  z
3433cv 1648 . . . . . . . . . . . . . . . 16  class  z
3532, 34, 12co 6013 . . . . . . . . . . . . . . 15  class  ( <.
x ,  y >.
o z )
363, 5, 35co 6013 . . . . . . . . . . . . . 14  class  ( g ( <. x ,  y
>. o z ) f )
379, 34, 17co 6013 . . . . . . . . . . . . . 14  class  ( x h z )
3836, 37wcel 1717 . . . . . . . . . . . . 13  wff  ( g ( <. x ,  y
>. o z ) f )  e.  ( x h z )
39 vk . . . . . . . . . . . . . . . . . . 19  set  k
4039cv 1648 . . . . . . . . . . . . . . . . . 18  class  k
417, 34cop 3753 . . . . . . . . . . . . . . . . . . 19  class  <. y ,  z >.
42 vw . . . . . . . . . . . . . . . . . . . 20  set  w
4342cv 1648 . . . . . . . . . . . . . . . . . . 19  class  w
4441, 43, 12co 6013 . . . . . . . . . . . . . . . . . 18  class  ( <.
y ,  z >.
o w )
4540, 3, 44co 6013 . . . . . . . . . . . . . . . . 17  class  ( k ( <. y ,  z
>. o w ) g )
4632, 43, 12co 6013 . . . . . . . . . . . . . . . . 17  class  ( <.
x ,  y >.
o w )
4745, 5, 46co 6013 . . . . . . . . . . . . . . . 16  class  ( ( k ( <. y ,  z >. o
w ) g ) ( <. x ,  y
>. o w ) f )
489, 34cop 3753 . . . . . . . . . . . . . . . . . 18  class  <. x ,  z >.
4948, 43, 12co 6013 . . . . . . . . . . . . . . . . 17  class  ( <.
x ,  z >.
o w )
5040, 36, 49co 6013 . . . . . . . . . . . . . . . 16  class  ( k ( <. x ,  z
>. o w ) ( g ( <. x ,  y >. o
z ) f ) )
5147, 50wceq 1649 . . . . . . . . . . . . . . 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 6013 . . . . . . . . . . . . . . 15  class  ( z h w )
5351, 39, 52wral 2642 . . . . . . . . . . . . . 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 2642 . . . . . . . . . . . . 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 359 . . . . . . . . . . . 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 6013 . . . . . . . . . . . 12  class  ( y h z )
5755, 2, 56wral 2642 . . . . . . . . . . 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 2642 . . . . . . . . . 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 2642 . . . . . . . . 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 2642 . . . . . . . 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 359 . . . . . . 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 2642 . . . . . 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  set  c
6463cv 1648 . . . . . . 7  class  c
65 cco 13461 . . . . . . 7  class comp
6664, 65cfv 5387 . . . . . 6  class  (comp `  c )
6762, 11, 66wsbc 3097 . . . . 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 13460 . . . . . 6  class  Hom
6964, 68cfv 5387 . . . . 5  class  (  Hom  `  c )
7067, 16, 69wsbc 3097 . . . 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 13389 . . . . 5  class  Base
7264, 71cfv 5387 . . . 4  class  ( Base `  c )
7370, 27, 72wsbc 3097 . . 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 2366 . 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 1649 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 set class
This definition is referenced by:  iscat  13817
  Copyright terms: Public domain W3C validator