Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-catOLD Unicode version

Definition df-catOLD 25753
Description: A category is a deductive system where composition is associative, and identities are neutral elements. 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.)
Assertion
Ref Expression
df-catOLD  |-  Cat OLD  =  { x  |  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) ) ) }
Distinct variable group:    x, d, c, j, r, f, g, h, a

Detailed syntax breakdown of Definition df-catOLD
StepHypRef Expression
1 ccatOLD 25752 . 2  class  Cat OLD
2 vx . . . . . . . . . 10  set  x
32cv 1622 . . . . . . . . 9  class  x
4 vd . . . . . . . . . . . 12  set  d
54cv 1622 . . . . . . . . . . 11  class  d
6 vc . . . . . . . . . . . 12  set  c
76cv 1622 . . . . . . . . . . 11  class  c
85, 7cop 3643 . . . . . . . . . 10  class  <. d ,  c >.
9 vj . . . . . . . . . . . 12  set  j
109cv 1622 . . . . . . . . . . 11  class  j
11 vr . . . . . . . . . . . 12  set  r
1211cv 1622 . . . . . . . . . . 11  class  r
1310, 12cop 3643 . . . . . . . . . 10  class  <. j ,  r >.
148, 13cop 3643 . . . . . . . . 9  class  <. <. d ,  c >. ,  <. j ,  r >. >.
153, 14wceq 1623 . . . . . . . 8  wff  x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.
16 cded 25734 . . . . . . . . . . 11  class  Ded
1714, 16wcel 1684 . . . . . . . . . 10  wff  <. <. d ,  c >. ,  <. j ,  r >. >.  e.  Ded
18 vh . . . . . . . . . . . . . . . . . 18  set  h
1918cv 1622 . . . . . . . . . . . . . . . . 17  class  h
2019, 5cfv 5255 . . . . . . . . . . . . . . . 16  class  ( d `
 h )
21 vg . . . . . . . . . . . . . . . . . 18  set  g
2221cv 1622 . . . . . . . . . . . . . . . . 17  class  g
2322, 7cfv 5255 . . . . . . . . . . . . . . . 16  class  ( c `
 g )
2420, 23wceq 1623 . . . . . . . . . . . . . . 15  wff  ( d `
 h )  =  ( c `  g
)
2522, 5cfv 5255 . . . . . . . . . . . . . . . 16  class  ( d `
 g )
26 vf . . . . . . . . . . . . . . . . . 18  set  f
2726cv 1622 . . . . . . . . . . . . . . . . 17  class  f
2827, 7cfv 5255 . . . . . . . . . . . . . . . 16  class  ( c `
 f )
2925, 28wceq 1623 . . . . . . . . . . . . . . 15  wff  ( d `
 g )  =  ( c `  f
)
3024, 29wa 358 . . . . . . . . . . . . . 14  wff  ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )
3122, 27, 12co 5858 . . . . . . . . . . . . . . . 16  class  ( g r f )
3219, 31, 12co 5858 . . . . . . . . . . . . . . 15  class  ( h r ( g r f ) )
3319, 22, 12co 5858 . . . . . . . . . . . . . . . 16  class  ( h r g )
3433, 27, 12co 5858 . . . . . . . . . . . . . . 15  class  ( ( h r g ) r f )
3532, 34wceq 1623 . . . . . . . . . . . . . 14  wff  ( h r ( g r f ) )  =  ( ( h r g ) r f )
3630, 35wi 4 . . . . . . . . . . . . 13  wff  ( ( ( d `  h
)  =  ( c `
 g )  /\  ( d `  g
)  =  ( c `
 f ) )  ->  ( h r ( g r f ) )  =  ( ( h r g ) r f ) )
375cdm 4689 . . . . . . . . . . . . 13  class  dom  d
3836, 18, 37wral 2543 . . . . . . . . . . . 12  wff  A. h  e.  dom  d ( ( ( d `  h
)  =  ( c `
 g )  /\  ( d `  g
)  =  ( c `
 f ) )  ->  ( h r ( g r f ) )  =  ( ( h r g ) r f ) )
3938, 21, 37wral 2543 . . . . . . . . . . 11  wff  A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h
)  =  ( c `
 g )  /\  ( d `  g
)  =  ( c `
 f ) )  ->  ( h r ( g r f ) )  =  ( ( h r g ) r f ) )
4039, 26, 37wral 2543 . . . . . . . . . 10  wff  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h
)  =  ( c `
 g )  /\  ( d `  g
)  =  ( c `
 f ) )  ->  ( h r ( g r f ) )  =  ( ( h r g ) r f ) )
4117, 40wa 358 . . . . . . . . 9  wff  ( <. <. d ,  c >. ,  <. j ,  r
>. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )
42 va . . . . . . . . . . . . . . 15  set  a
4342cv 1622 . . . . . . . . . . . . . 14  class  a
4428, 43wceq 1623 . . . . . . . . . . . . 13  wff  ( c `
 f )  =  a
4543, 10cfv 5255 . . . . . . . . . . . . . . 15  class  ( j `
 a )
4645, 27, 12co 5858 . . . . . . . . . . . . . 14  class  ( ( j `  a ) r f )
4746, 27wceq 1623 . . . . . . . . . . . . 13  wff  ( ( j `  a ) r f )  =  f
4844, 47wi 4 . . . . . . . . . . . 12  wff  ( ( c `  f )  =  a  ->  (
( j `  a
) r f )  =  f )
4948, 26, 37wral 2543 . . . . . . . . . . 11  wff  A. f  e.  dom  d ( ( c `  f )  =  a  ->  (
( j `  a
) r f )  =  f )
5010cdm 4689 . . . . . . . . . . 11  class  dom  j
5149, 42, 50wral 2543 . . . . . . . . . 10  wff  A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f )  =  a  ->  (
( j `  a
) r f )  =  f )
5227, 5cfv 5255 . . . . . . . . . . . . . 14  class  ( d `
 f )
5352, 43wceq 1623 . . . . . . . . . . . . 13  wff  ( d `
 f )  =  a
5427, 45, 12co 5858 . . . . . . . . . . . . . 14  class  ( f r ( j `  a ) )
5554, 27wceq 1623 . . . . . . . . . . . . 13  wff  ( f r ( j `  a ) )  =  f
5653, 55wi 4 . . . . . . . . . . . 12  wff  ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f )
5756, 26, 37wral 2543 . . . . . . . . . . 11  wff  A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f )
5857, 42, 50wral 2543 . . . . . . . . . 10  wff  A. a  e.  dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f )
5951, 58wa 358 . . . . . . . . 9  wff  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) )
6041, 59wa 358 . . . . . . . 8  wff  ( (
<. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) )
6115, 60wa 358 . . . . . . 7  wff  ( x  =  <. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) ) )
6261, 11wex 1528 . . . . . 6  wff  E. r
( x  =  <. <.
d ,  c >. ,  <. j ,  r
>. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) ) )
6362, 9wex 1528 . . . . 5  wff  E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) ) )
6463, 6wex 1528 . . . 4  wff  E. c E. j E. r ( x  =  <. <. d ,  c >. ,  <. j ,  r >. >.  /\  (
( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) ) )
6564, 4wex 1528 . . 3  wff  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) ) )
6665, 2cab 2269 . 2  class  { x  |  E. d E. c E. j E. r ( x  =  <. <. d ,  c >. ,  <. j ,  r >. >.  /\  (
( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) ) ) }
671, 66wceq 1623 1  wff  Cat OLD  =  { x  |  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Ded  /\  A. f  e.  dom  d A. g  e.  dom  d A. h  e.  dom  d ( ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )  -> 
( h r ( g r f ) )  =  ( ( h r g ) r f ) ) )  /\  ( A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f
)  =  a  -> 
( ( j `  a ) r f )  =  f )  /\  A. a  e. 
dom  j A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  iscatOLD  25754  cati  25755  strcat  25760
  Copyright terms: Public domain W3C validator