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 25856
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 25855 . 2  class  Cat OLD
2 vx . . . . . . . . . 10  set  x
32cv 1631 . . . . . . . . 9  class  x
4 vd . . . . . . . . . . . 12  set  d
54cv 1631 . . . . . . . . . . 11  class  d
6 vc . . . . . . . . . . . 12  set  c
76cv 1631 . . . . . . . . . . 11  class  c
85, 7cop 3656 . . . . . . . . . 10  class  <. d ,  c >.
9 vj . . . . . . . . . . . 12  set  j
109cv 1631 . . . . . . . . . . 11  class  j
11 vr . . . . . . . . . . . 12  set  r
1211cv 1631 . . . . . . . . . . 11  class  r
1310, 12cop 3656 . . . . . . . . . 10  class  <. j ,  r >.
148, 13cop 3656 . . . . . . . . 9  class  <. <. d ,  c >. ,  <. j ,  r >. >.
153, 14wceq 1632 . . . . . . . 8  wff  x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.
16 cded 25837 . . . . . . . . . . 11  class  Ded
1714, 16wcel 1696 . . . . . . . . . 10  wff  <. <. d ,  c >. ,  <. j ,  r >. >.  e.  Ded
18 vh . . . . . . . . . . . . . . . . . 18  set  h
1918cv 1631 . . . . . . . . . . . . . . . . 17  class  h
2019, 5cfv 5271 . . . . . . . . . . . . . . . 16  class  ( d `
 h )
21 vg . . . . . . . . . . . . . . . . . 18  set  g
2221cv 1631 . . . . . . . . . . . . . . . . 17  class  g
2322, 7cfv 5271 . . . . . . . . . . . . . . . 16  class  ( c `
 g )
2420, 23wceq 1632 . . . . . . . . . . . . . . 15  wff  ( d `
 h )  =  ( c `  g
)
2522, 5cfv 5271 . . . . . . . . . . . . . . . 16  class  ( d `
 g )
26 vf . . . . . . . . . . . . . . . . . 18  set  f
2726cv 1631 . . . . . . . . . . . . . . . . 17  class  f
2827, 7cfv 5271 . . . . . . . . . . . . . . . 16  class  ( c `
 f )
2925, 28wceq 1632 . . . . . . . . . . . . . . 15  wff  ( d `
 g )  =  ( c `  f
)
3024, 29wa 358 . . . . . . . . . . . . . 14  wff  ( ( d `  h )  =  ( c `  g )  /\  (
d `  g )  =  ( c `  f ) )
3122, 27, 12co 5874 . . . . . . . . . . . . . . . 16  class  ( g r f )
3219, 31, 12co 5874 . . . . . . . . . . . . . . 15  class  ( h r ( g r f ) )
3319, 22, 12co 5874 . . . . . . . . . . . . . . . 16  class  ( h r g )
3433, 27, 12co 5874 . . . . . . . . . . . . . . 15  class  ( ( h r g ) r f )
3532, 34wceq 1632 . . . . . . . . . . . . . 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 4705 . . . . . . . . . . . . 13  class  dom  d
3836, 18, 37wral 2556 . . . . . . . . . . . 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 2556 . . . . . . . . . . 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 2556 . . . . . . . . . 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 1631 . . . . . . . . . . . . . 14  class  a
4428, 43wceq 1632 . . . . . . . . . . . . 13  wff  ( c `
 f )  =  a
4543, 10cfv 5271 . . . . . . . . . . . . . . 15  class  ( j `
 a )
4645, 27, 12co 5874 . . . . . . . . . . . . . 14  class  ( ( j `  a ) r f )
4746, 27wceq 1632 . . . . . . . . . . . . 13  wff  ( ( j `  a ) r f )  =  f
4844, 47wi 4 . . . . . . . . . . . 12  wff  ( ( c `  f )  =  a  ->  (
( j `  a
) r f )  =  f )
4948, 26, 37wral 2556 . . . . . . . . . . 11  wff  A. f  e.  dom  d ( ( c `  f )  =  a  ->  (
( j `  a
) r f )  =  f )
5010cdm 4705 . . . . . . . . . . 11  class  dom  j
5149, 42, 50wral 2556 . . . . . . . . . 10  wff  A. a  e.  dom  j A. f  e.  dom  d ( ( c `  f )  =  a  ->  (
( j `  a
) r f )  =  f )
5227, 5cfv 5271 . . . . . . . . . . . . . 14  class  ( d `
 f )
5352, 43wceq 1632 . . . . . . . . . . . . 13  wff  ( d `
 f )  =  a
5427, 45, 12co 5874 . . . . . . . . . . . . . 14  class  ( f r ( j `  a ) )
5554, 27wceq 1632 . . . . . . . . . . . . 13  wff  ( f r ( j `  a ) )  =  f
5653, 55wi 4 . . . . . . . . . . . 12  wff  ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f )
5756, 26, 37wral 2556 . . . . . . . . . . 11  wff  A. f  e.  dom  d ( ( d `  f )  =  a  ->  (
f r ( j `
 a ) )  =  f )
5857, 42, 50wral 2556 . . . . . . . . . 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 1531 . . . . . 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 1531 . . . . 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 1531 . . . 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 1531 . . 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 2282 . 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 1632 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  25857  cati  25858  strcat  25863
  Copyright terms: Public domain W3C validator