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

Definition df-ded 25735
Description: Definition of a deductive system. Lambeck and Scott. Introduction to higher order categorical logic. p. 47. 1986. Unformally we can say a deductive system is a directed multi graph where for each object a specific morphism called identity of the object exists and where for some pairs of morphisms the composite exists. Deductive system are named so because morphisms may be interpreted as logical deductions, objects as sets of formulas and compositions as inferences. (Contributed by FL, 24-Oct-2007.)
Assertion
Ref Expression
df-ded  |-  Ded  =  { x  |  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) ) ) }
Distinct variable group:    x, d, c, j, r, a, f, g

Detailed syntax breakdown of Definition df-ded
StepHypRef Expression
1 cded 25734 . 2  class  Ded
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 calg 25711 . . . . . . . . . . 11  class  Alg
1714, 16wcel 1684 . . . . . . . . . 10  wff  <. <. d ,  c >. ,  <. j ,  r >. >.  e.  Alg
18 va . . . . . . . . . . . . . . . 16  set  a
1918cv 1622 . . . . . . . . . . . . . . 15  class  a
2019, 10cfv 5255 . . . . . . . . . . . . . 14  class  ( j `
 a )
2120, 5cfv 5255 . . . . . . . . . . . . 13  class  ( d `
 ( j `  a ) )
2221, 19wceq 1623 . . . . . . . . . . . 12  wff  ( d `
 ( j `  a ) )  =  a
2320, 7cfv 5255 . . . . . . . . . . . . 13  class  ( c `
 ( j `  a ) )
2423, 19wceq 1623 . . . . . . . . . . . 12  wff  ( c `
 ( j `  a ) )  =  a
2522, 24wa 358 . . . . . . . . . . 11  wff  ( ( d `  ( j `
 a ) )  =  a  /\  (
c `  ( j `  a ) )  =  a )
2610cdm 4689 . . . . . . . . . . 11  class  dom  j
2725, 18, 26wral 2543 . . . . . . . . . 10  wff  A. a  e.  dom  j ( ( d `  ( j `
 a ) )  =  a  /\  (
c `  ( j `  a ) )  =  a )
28 vg . . . . . . . . . . . . . . . 16  set  g
2928cv 1622 . . . . . . . . . . . . . . 15  class  g
30 vf . . . . . . . . . . . . . . . 16  set  f
3130cv 1622 . . . . . . . . . . . . . . 15  class  f
3229, 31cop 3643 . . . . . . . . . . . . . 14  class  <. g ,  f >.
3312cdm 4689 . . . . . . . . . . . . . 14  class  dom  r
3432, 33wcel 1684 . . . . . . . . . . . . 13  wff  <. g ,  f >.  e.  dom  r
3529, 5cfv 5255 . . . . . . . . . . . . . 14  class  ( d `
 g )
3631, 7cfv 5255 . . . . . . . . . . . . . 14  class  ( c `
 f )
3735, 36wceq 1623 . . . . . . . . . . . . 13  wff  ( d `
 g )  =  ( c `  f
)
3834, 37wb 176 . . . . . . . . . . . 12  wff  ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) )
395cdm 4689 . . . . . . . . . . . 12  class  dom  d
4038, 28, 39wral 2543 . . . . . . . . . . 11  wff  A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) )
4140, 30, 39wral 2543 . . . . . . . . . 10  wff  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) )
4217, 27, 41w3a 934 . . . . . . . . 9  wff  ( <. <. d ,  c >. ,  <. j ,  r
>. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )
4329, 31, 12co 5858 . . . . . . . . . . . . . . 15  class  ( g r f )
4443, 5cfv 5255 . . . . . . . . . . . . . 14  class  ( d `
 ( g r f ) )
4531, 5cfv 5255 . . . . . . . . . . . . . 14  class  ( d `
 f )
4644, 45wceq 1623 . . . . . . . . . . . . 13  wff  ( d `
 ( g r f ) )  =  ( d `  f
)
4737, 46wi 4 . . . . . . . . . . . 12  wff  ( ( d `  g )  =  ( c `  f )  ->  (
d `  ( g
r f ) )  =  ( d `  f ) )
4847, 28, 39wral 2543 . . . . . . . . . . 11  wff  A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
d `  ( g
r f ) )  =  ( d `  f ) )
4948, 30, 39wral 2543 . . . . . . . . . 10  wff  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
d `  ( g
r f ) )  =  ( d `  f ) )
5043, 7cfv 5255 . . . . . . . . . . . . . 14  class  ( c `
 ( g r f ) )
5129, 7cfv 5255 . . . . . . . . . . . . . 14  class  ( c `
 g )
5250, 51wceq 1623 . . . . . . . . . . . . 13  wff  ( c `
 ( g r f ) )  =  ( c `  g
)
5337, 52wi 4 . . . . . . . . . . . 12  wff  ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) )
5453, 28, 39wral 2543 . . . . . . . . . . 11  wff  A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) )
5554, 30, 39wral 2543 . . . . . . . . . 10  wff  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) )
5649, 55wa 358 . . . . . . . . 9  wff  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g
)  =  ( c `
 f )  -> 
( d `  (
g r f ) )  =  ( d `
 f ) )  /\  A. f  e. 
dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) )
5742, 56wa 358 . . . . . . . 8  wff  ( (
<. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) )
5815, 57wa 358 . . . . . . 7  wff  ( x  =  <. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) ) )
5958, 11wex 1528 . . . . . 6  wff  E. r
( x  =  <. <.
d ,  c >. ,  <. j ,  r
>. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) ) )
6059, 9wex 1528 . . . . 5  wff  E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) ) )
6160, 6wex 1528 . . . 4  wff  E. c E. j E. r ( x  =  <. <. d ,  c >. ,  <. j ,  r >. >.  /\  (
( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) ) )
6261, 4wex 1528 . . 3  wff  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) ) )
6362, 2cab 2269 . 2  class  { x  |  E. d E. c E. j E. r ( x  =  <. <. d ,  c >. ,  <. j ,  r >. >.  /\  (
( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) ) ) }
641, 63wceq 1623 1  wff  Ded  =  { x  |  E. d E. c E. j E. r ( x  = 
<. <. d ,  c
>. ,  <. j ,  r >. >.  /\  ( ( <. <. d ,  c
>. ,  <. j ,  r >. >.  e.  Alg  /\  A. a  e.  dom  j
( ( d `  ( j `  a
) )  =  a  /\  ( c `  ( j `  a
) )  =  a )  /\  A. f  e.  dom  d A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) ) )  /\  ( A. f  e.  dom  d A. g  e.  dom  d ( ( d `
 g )  =  ( c `  f
)  ->  ( d `  ( g r f ) )  =  ( d `  f ) )  /\  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isded  25736  dedi  25737  strded  25739
  Copyright terms: Public domain W3C validator