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

Definition df-derv 26158
Description: The relation  u derives  v in one step in the grammar  g. Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-derv  |-  derv  =  ( g  e.  Grammar  |->  {
<. x ,  y >.  |  ( x  e.  ( Kleene `  g )  /\  y  e.  ( Kleene `
 g )  /\  E. u  e.  ( Kleene `  g ) E. v  e.  ( Kleene `  g ) E. p  e.  ( Kleene `
 g ) E. q  e.  ( Kleene `  g ) ( x  =  ( ( u (  conc  `  g ) p ) (  conc  `  g ) v )  /\  <. p ,  q
>.  e.  ( prdct `  g
)  /\  y  =  ( ( u ( 
conc  `  g ) q ) (  conc  `  g
) v ) ) ) } )
Distinct variable group:    x, g, y, u, v, p, q

Detailed syntax breakdown of Definition df-derv
StepHypRef Expression
1 cderv 26157 . 2  class  derv
2 vg . . 3  set  g
3 cgrm 26101 . . 3  class  Grammar
4 vx . . . . . . 7  set  x
54cv 1631 . . . . . 6  class  x
62cv 1631 . . . . . . 7  class  g
7 ckln 26083 . . . . . . 7  class  Kleene
86, 7cfv 5271 . . . . . 6  class  ( Kleene `  g )
95, 8wcel 1696 . . . . 5  wff  x  e.  ( Kleene `  g )
10 vy . . . . . . 7  set  y
1110cv 1631 . . . . . 6  class  y
1211, 8wcel 1696 . . . . 5  wff  y  e.  ( Kleene `  g )
13 vu . . . . . . . . . . . . . 14  set  u
1413cv 1631 . . . . . . . . . . . . 13  class  u
15 vp . . . . . . . . . . . . . 14  set  p
1615cv 1631 . . . . . . . . . . . . 13  class  p
17 cconc 26107 . . . . . . . . . . . . . 14  class  conc
186, 17cfv 5271 . . . . . . . . . . . . 13  class  (  conc  `  g )
1914, 16, 18co 5874 . . . . . . . . . . . 12  class  ( u (  conc  `  g ) p )
20 vv . . . . . . . . . . . . 13  set  v
2120cv 1631 . . . . . . . . . . . 12  class  v
2219, 21, 18co 5874 . . . . . . . . . . 11  class  ( ( u (  conc  `  g
) p ) ( 
conc  `  g ) v )
235, 22wceq 1632 . . . . . . . . . 10  wff  x  =  ( ( u ( 
conc  `  g ) p ) (  conc  `  g
) v )
24 vq . . . . . . . . . . . . 13  set  q
2524cv 1631 . . . . . . . . . . . 12  class  q
2616, 25cop 3656 . . . . . . . . . . 11  class  <. p ,  q >.
27 cprdct 26105 . . . . . . . . . . . 12  class  prdct
286, 27cfv 5271 . . . . . . . . . . 11  class  ( prdct `  g )
2926, 28wcel 1696 . . . . . . . . . 10  wff  <. p ,  q >.  e.  (
prdct `  g )
3014, 25, 18co 5874 . . . . . . . . . . . 12  class  ( u (  conc  `  g ) q )
3130, 21, 18co 5874 . . . . . . . . . . 11  class  ( ( u (  conc  `  g
) q ) ( 
conc  `  g ) v )
3211, 31wceq 1632 . . . . . . . . . 10  wff  y  =  ( ( u ( 
conc  `  g ) q ) (  conc  `  g
) v )
3323, 29, 32w3a 934 . . . . . . . . 9  wff  ( x  =  ( ( u (  conc  `  g ) p ) (  conc  `  g ) v )  /\  <. p ,  q
>.  e.  ( prdct `  g
)  /\  y  =  ( ( u ( 
conc  `  g ) q ) (  conc  `  g
) v ) )
3433, 24, 8wrex 2557 . . . . . . . 8  wff  E. q  e.  ( Kleene `  g )
( x  =  ( ( u (  conc  `  g ) p ) (  conc  `  g ) v )  /\  <. p ,  q >.  e.  (
prdct `  g )  /\  y  =  ( (
u (  conc  `  g
) q ) ( 
conc  `  g ) v ) )
3534, 15, 8wrex 2557 . . . . . . 7  wff  E. p  e.  ( Kleene `  g ) E. q  e.  ( Kleene `
 g ) ( x  =  ( ( u (  conc  `  g
) p ) ( 
conc  `  g ) v )  /\  <. p ,  q >.  e.  (
prdct `  g )  /\  y  =  ( (
u (  conc  `  g
) q ) ( 
conc  `  g ) v ) )
3635, 20, 8wrex 2557 . . . . . 6  wff  E. v  e.  ( Kleene `  g ) E. p  e.  ( Kleene `
 g ) E. q  e.  ( Kleene `  g ) ( x  =  ( ( u (  conc  `  g ) p ) (  conc  `  g ) v )  /\  <. p ,  q
>.  e.  ( prdct `  g
)  /\  y  =  ( ( u ( 
conc  `  g ) q ) (  conc  `  g
) v ) )
3736, 13, 8wrex 2557 . . . . 5  wff  E. u  e.  ( Kleene `  g ) E. v  e.  ( Kleene `
 g ) E. p  e.  ( Kleene `  g ) E. q  e.  ( Kleene `  g )
( x  =  ( ( u (  conc  `  g ) p ) (  conc  `  g ) v )  /\  <. p ,  q >.  e.  (
prdct `  g )  /\  y  =  ( (
u (  conc  `  g
) q ) ( 
conc  `  g ) v ) )
389, 12, 37w3a 934 . . . 4  wff  ( x  e.  ( Kleene `  g
)  /\  y  e.  ( Kleene `  g )  /\  E. u  e.  (
Kleene `  g ) E. v  e.  ( Kleene `  g ) E. p  e.  ( Kleene `  g ) E. q  e.  ( Kleene `
 g ) ( x  =  ( ( u (  conc  `  g
) p ) ( 
conc  `  g ) v )  /\  <. p ,  q >.  e.  (
prdct `  g )  /\  y  =  ( (
u (  conc  `  g
) q ) ( 
conc  `  g ) v ) ) )
3938, 4, 10copab 4092 . . 3  class  { <. x ,  y >.  |  ( x  e.  ( Kleene `  g )  /\  y  e.  ( Kleene `  g )  /\  E. u  e.  (
Kleene `  g ) E. v  e.  ( Kleene `  g ) E. p  e.  ( Kleene `  g ) E. q  e.  ( Kleene `
 g ) ( x  =  ( ( u (  conc  `  g
) p ) ( 
conc  `  g ) v )  /\  <. p ,  q >.  e.  (
prdct `  g )  /\  y  =  ( (
u (  conc  `  g
) q ) ( 
conc  `  g ) v ) ) ) }
402, 3, 39cmpt 4093 . 2  class  ( g  e.  Grammar  |->  { <. x ,  y >.  |  ( x  e.  ( Kleene `  g )  /\  y  e.  ( Kleene `  g )  /\  E. u  e.  (
Kleene `  g ) E. v  e.  ( Kleene `  g ) E. p  e.  ( Kleene `  g ) E. q  e.  ( Kleene `
 g ) ( x  =  ( ( u (  conc  `  g
) p ) ( 
conc  `  g ) v )  /\  <. p ,  q >.  e.  (
prdct `  g )  /\  y  =  ( (
u (  conc  `  g
) q ) ( 
conc  `  g ) v ) ) ) } )
411, 40wceq 1632 1  wff  derv  =  ( g  e.  Grammar  |->  {
<. x ,  y >.  |  ( x  e.  ( Kleene `  g )  /\  y  e.  ( Kleene `
 g )  /\  E. u  e.  ( Kleene `  g ) E. v  e.  ( Kleene `  g ) E. p  e.  ( Kleene `
 g ) E. q  e.  ( Kleene `  g ) ( x  =  ( ( u (  conc  `  g ) p ) (  conc  `  g ) v )  /\  <. p ,  q
>.  e.  ( prdct `  g
)  /\  y  =  ( ( u ( 
conc  `  g ) q ) (  conc  `  g
) v ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator