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 25838
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 25837 . 2  class  Ded
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 calg 25814 . . . . . . . . . . 11  class  Alg
1714, 16wcel 1696 . . . . . . . . . 10  wff  <. <. d ,  c >. ,  <. j ,  r >. >.  e.  Alg
18 va . . . . . . . . . . . . . . . 16  set  a
1918cv 1631 . . . . . . . . . . . . . . 15  class  a
2019, 10cfv 5271 . . . . . . . . . . . . . 14  class  ( j `
 a )
2120, 5cfv 5271 . . . . . . . . . . . . 13  class  ( d `
 ( j `  a ) )
2221, 19wceq 1632 . . . . . . . . . . . 12  wff  ( d `
 ( j `  a ) )  =  a
2320, 7cfv 5271 . . . . . . . . . . . . 13  class  ( c `
 ( j `  a ) )
2423, 19wceq 1632 . . . . . . . . . . . 12  wff  ( c `
 ( j `  a ) )  =  a
2522, 24wa 358 . . . . . . . . . . 11  wff  ( ( d `  ( j `
 a ) )  =  a  /\  (
c `  ( j `  a ) )  =  a )
2610cdm 4705 . . . . . . . . . . 11  class  dom  j
2725, 18, 26wral 2556 . . . . . . . . . 10  wff  A. a  e.  dom  j ( ( d `  ( j `
 a ) )  =  a  /\  (
c `  ( j `  a ) )  =  a )
28 vg . . . . . . . . . . . . . . . 16  set  g
2928cv 1631 . . . . . . . . . . . . . . 15  class  g
30 vf . . . . . . . . . . . . . . . 16  set  f
3130cv 1631 . . . . . . . . . . . . . . 15  class  f
3229, 31cop 3656 . . . . . . . . . . . . . 14  class  <. g ,  f >.
3312cdm 4705 . . . . . . . . . . . . . 14  class  dom  r
3432, 33wcel 1696 . . . . . . . . . . . . 13  wff  <. g ,  f >.  e.  dom  r
3529, 5cfv 5271 . . . . . . . . . . . . . 14  class  ( d `
 g )
3631, 7cfv 5271 . . . . . . . . . . . . . 14  class  ( c `
 f )
3735, 36wceq 1632 . . . . . . . . . . . . 13  wff  ( d `
 g )  =  ( c `  f
)
3834, 37wb 176 . . . . . . . . . . . 12  wff  ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) )
395cdm 4705 . . . . . . . . . . . 12  class  dom  d
4038, 28, 39wral 2556 . . . . . . . . . . 11  wff  A. g  e.  dom  d ( <.
g ,  f >.  e.  dom  r  <->  ( d `  g )  =  ( c `  f ) )
4140, 30, 39wral 2556 . . . . . . . . . 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 5874 . . . . . . . . . . . . . . 15  class  ( g r f )
4443, 5cfv 5271 . . . . . . . . . . . . . 14  class  ( d `
 ( g r f ) )
4531, 5cfv 5271 . . . . . . . . . . . . . 14  class  ( d `
 f )
4644, 45wceq 1632 . . . . . . . . . . . . 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 2556 . . . . . . . . . . 11  wff  A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
d `  ( g
r f ) )  =  ( d `  f ) )
4948, 30, 39wral 2556 . . . . . . . . . 10  wff  A. f  e.  dom  d A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
d `  ( g
r f ) )  =  ( d `  f ) )
5043, 7cfv 5271 . . . . . . . . . . . . . 14  class  ( c `
 ( g r f ) )
5129, 7cfv 5271 . . . . . . . . . . . . . 14  class  ( c `
 g )
5250, 51wceq 1632 . . . . . . . . . . . . 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 2556 . . . . . . . . . . 11  wff  A. g  e.  dom  d ( ( d `  g )  =  ( c `  f )  ->  (
c `  ( g
r f ) )  =  ( c `  g ) )
5554, 30, 39wral 2556 . . . . . . . . . 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 1531 . . . . . 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 1531 . . . . 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 1531 . . . 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 1531 . . 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 2282 . 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 1632 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  25839  dedi  25840  strded  25842
  Copyright terms: Public domain W3C validator