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

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