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

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