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

Definition df-cat 14598
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 14594 . 2  class  Cat
2 vg . . . . . . . . . . . . . . 15  setvar  g
32cv 1368 . . . . . . . . . . . . . 14  class  g
4 vf . . . . . . . . . . . . . . 15  setvar  f
54cv 1368 . . . . . . . . . . . . . 14  class  f
6 vy . . . . . . . . . . . . . . . . 17  setvar  y
76cv 1368 . . . . . . . . . . . . . . . 16  class  y
8 vx . . . . . . . . . . . . . . . . 17  setvar  x
98cv 1368 . . . . . . . . . . . . . . . 16  class  x
107, 9cop 3878 . . . . . . . . . . . . . . 15  class  <. y ,  x >.
11 vo . . . . . . . . . . . . . . . 16  setvar  o
1211cv 1368 . . . . . . . . . . . . . . 15  class  o
1310, 9, 12co 6086 . . . . . . . . . . . . . 14  class  ( <.
y ,  x >. o x )
143, 5, 13co 6086 . . . . . . . . . . . . 13  class  ( g ( <. y ,  x >. o x ) f )
1514, 5wceq 1369 . . . . . . . . . . . 12  wff  ( g ( <. y ,  x >. o x ) f )  =  f
16 vh . . . . . . . . . . . . . 14  setvar  h
1716cv 1368 . . . . . . . . . . . . 13  class  h
187, 9, 17co 6086 . . . . . . . . . . . 12  class  ( y h x )
1915, 4, 18wral 2710 . . . . . . . . . . 11  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
209, 9cop 3878 . . . . . . . . . . . . . . 15  class  <. x ,  x >.
2120, 7, 12co 6086 . . . . . . . . . . . . . 14  class  ( <.
x ,  x >. o y )
225, 3, 21co 6086 . . . . . . . . . . . . 13  class  ( f ( <. x ,  x >. o y ) g )
2322, 5wceq 1369 . . . . . . . . . . . 12  wff  ( f ( <. x ,  x >. o y ) g )  =  f
249, 7, 17co 6086 . . . . . . . . . . . 12  class  ( x h y )
2523, 4, 24wral 2710 . . . . . . . . . . 11  wff  A. f  e.  ( x h y ) ( f (
<. x ,  x >. o y ) g )  =  f
2619, 25wa 369 . . . . . . . . . 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 1368 . . . . . . . . . 10  class  b
2926, 6, 28wral 2710 . . . . . . . . 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 6086 . . . . . . . . 9  class  ( x h x )
3129, 2, 30wrex 2711 . . . . . . . 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 3878 . . . . . . . . . . . . . . . 16  class  <. x ,  y >.
33 vz . . . . . . . . . . . . . . . . 17  setvar  z
3433cv 1368 . . . . . . . . . . . . . . . 16  class  z
3532, 34, 12co 6086 . . . . . . . . . . . . . . 15  class  ( <.
x ,  y >.
o z )
363, 5, 35co 6086 . . . . . . . . . . . . . 14  class  ( g ( <. x ,  y
>. o z ) f )
379, 34, 17co 6086 . . . . . . . . . . . . . 14  class  ( x h z )
3836, 37wcel 1756 . . . . . . . . . . . . 13  wff  ( g ( <. x ,  y
>. o z ) f )  e.  ( x h z )
39 vk . . . . . . . . . . . . . . . . . . 19  setvar  k
4039cv 1368 . . . . . . . . . . . . . . . . . 18  class  k
417, 34cop 3878 . . . . . . . . . . . . . . . . . . 19  class  <. y ,  z >.
42 vw . . . . . . . . . . . . . . . . . . . 20  setvar  w
4342cv 1368 . . . . . . . . . . . . . . . . . . 19  class  w
4441, 43, 12co 6086 . . . . . . . . . . . . . . . . . 18  class  ( <.
y ,  z >.
o w )
4540, 3, 44co 6086 . . . . . . . . . . . . . . . . 17  class  ( k ( <. y ,  z
>. o w ) g )
4632, 43, 12co 6086 . . . . . . . . . . . . . . . . 17  class  ( <.
x ,  y >.
o w )
4745, 5, 46co 6086 . . . . . . . . . . . . . . . 16  class  ( ( k ( <. y ,  z >. o
w ) g ) ( <. x ,  y
>. o w ) f )
489, 34cop 3878 . . . . . . . . . . . . . . . . . 18  class  <. x ,  z >.
4948, 43, 12co 6086 . . . . . . . . . . . . . . . . 17  class  ( <.
x ,  z >.
o w )
5040, 36, 49co 6086 . . . . . . . . . . . . . . . 16  class  ( k ( <. x ,  z
>. o w ) ( g ( <. x ,  y >. o
z ) f ) )
5147, 50wceq 1369 . . . . . . . . . . . . . . 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 6086 . . . . . . . . . . . . . . 15  class  ( z h w )
5351, 39, 52wral 2710 . . . . . . . . . . . . . 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 2710 . . . . . . . . . . . . 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 369 . . . . . . . . . . . 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 6086 . . . . . . . . . . . 12  class  ( y h z )
5755, 2, 56wral 2710 . . . . . . . . . . 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 2710 . . . . . . . . . 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 2710 . . . . . . . . 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 2710 . . . . . . . 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 369 . . . . . . 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 2710 . . . . . 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 1368 . . . . . . 7  class  c
65 cco 14242 . . . . . . 7  class comp
6664, 65cfv 5413 . . . . . 6  class  (comp `  c )
6762, 11, 66wsbc 3181 . . . . 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 14241 . . . . . 6  class  Hom
6964, 68cfv 5413 . . . . 5  class  ( Hom  `  c )
7067, 16, 69wsbc 3181 . . . 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 14166 . . . . 5  class  Base
7264, 71cfv 5413 . . . 4  class  ( Base `  c )
7370, 27, 72wsbc 3181 . . 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 2424 . 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 1369 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  14602
  Copyright terms: Public domain W3C validator