Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-msr Structured version   Unicode version

Definition df-msr 29961
Description: Define the reduct of a pre-statement. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-msr  |- mStRed  =  ( t  e.  _V  |->  ( s  e.  (mPreSt `  t )  |->  [_ ( 2nd `  ( 1st `  s
) )  /  h ]_ [_ ( 2nd `  s
)  /  a ]_ <. ( ( 1st `  ( 1st `  s ) )  i^i  [_ U. ( (mVars `  t ) " (
h  u.  { a } ) )  / 
z ]_ ( z  X.  z ) ) ,  h ,  a >.
) )
Distinct variable group:    h, a, s, t, z

Detailed syntax breakdown of Definition df-msr
StepHypRef Expression
1 cmsr 29941 . 2  class mStRed
2 vt . . 3  setvar  t
3 cvv 3078 . . 3  class  _V
4 vs . . . 4  setvar  s
52cv 1436 . . . . 5  class  t
6 cmpst 29940 . . . . 5  class mPreSt
75, 6cfv 5592 . . . 4  class  (mPreSt `  t )
8 vh . . . . 5  setvar  h
94cv 1436 . . . . . . 7  class  s
10 c1st 6796 . . . . . . 7  class  1st
119, 10cfv 5592 . . . . . 6  class  ( 1st `  s )
12 c2nd 6797 . . . . . 6  class  2nd
1311, 12cfv 5592 . . . . 5  class  ( 2nd `  ( 1st `  s
) )
14 va . . . . . 6  setvar  a
159, 12cfv 5592 . . . . . 6  class  ( 2nd `  s )
1611, 10cfv 5592 . . . . . . . 8  class  ( 1st `  ( 1st `  s
) )
17 vz . . . . . . . . 9  setvar  z
18 cmvrs 29936 . . . . . . . . . . . 12  class mVars
195, 18cfv 5592 . . . . . . . . . . 11  class  (mVars `  t )
208cv 1436 . . . . . . . . . . . 12  class  h
2114cv 1436 . . . . . . . . . . . . 13  class  a
2221csn 3993 . . . . . . . . . . . 12  class  { a }
2320, 22cun 3431 . . . . . . . . . . 11  class  ( h  u.  { a } )
2419, 23cima 4848 . . . . . . . . . 10  class  ( (mVars `  t ) " (
h  u.  { a } ) )
2524cuni 4213 . . . . . . . . 9  class  U. (
(mVars `  t ) " ( h  u. 
{ a } ) )
2617cv 1436 . . . . . . . . . 10  class  z
2726, 26cxp 4843 . . . . . . . . 9  class  ( z  X.  z )
2817, 25, 27csb 3392 . . . . . . . 8  class  [_ U. ( (mVars `  t ) " ( h  u. 
{ a } ) )  /  z ]_ ( z  X.  z
)
2916, 28cin 3432 . . . . . . 7  class  ( ( 1st `  ( 1st `  s ) )  i^i  [_ U. ( (mVars `  t ) " (
h  u.  { a } ) )  / 
z ]_ ( z  X.  z ) )
3029, 20, 21cotp 4001 . . . . . 6  class  <. (
( 1st `  ( 1st `  s ) )  i^i  [_ U. ( (mVars `  t ) " (
h  u.  { a } ) )  / 
z ]_ ( z  X.  z ) ) ,  h ,  a >.
3114, 15, 30csb 3392 . . . . 5  class  [_ ( 2nd `  s )  / 
a ]_ <. ( ( 1st `  ( 1st `  s
) )  i^i  [_ U. ( (mVars `  t ) " ( h  u. 
{ a } ) )  /  z ]_ ( z  X.  z
) ) ,  h ,  a >.
328, 13, 31csb 3392 . . . 4  class  [_ ( 2nd `  ( 1st `  s
) )  /  h ]_ [_ ( 2nd `  s
)  /  a ]_ <. ( ( 1st `  ( 1st `  s ) )  i^i  [_ U. ( (mVars `  t ) " (
h  u.  { a } ) )  / 
z ]_ ( z  X.  z ) ) ,  h ,  a >.
334, 7, 32cmpt 4475 . . 3  class  ( s  e.  (mPreSt `  t
)  |->  [_ ( 2nd `  ( 1st `  s ) )  /  h ]_ [_ ( 2nd `  s )  / 
a ]_ <. ( ( 1st `  ( 1st `  s
) )  i^i  [_ U. ( (mVars `  t ) " ( h  u. 
{ a } ) )  /  z ]_ ( z  X.  z
) ) ,  h ,  a >. )
342, 3, 33cmpt 4475 . 2  class  ( t  e.  _V  |->  ( s  e.  (mPreSt `  t
)  |->  [_ ( 2nd `  ( 1st `  s ) )  /  h ]_ [_ ( 2nd `  s )  / 
a ]_ <. ( ( 1st `  ( 1st `  s
) )  i^i  [_ U. ( (mVars `  t ) " ( h  u. 
{ a } ) )  /  z ]_ ( z  X.  z
) ) ,  h ,  a >. )
)
351, 34wceq 1437 1  wff mStRed  =  ( t  e.  _V  |->  ( s  e.  (mPreSt `  t )  |->  [_ ( 2nd `  ( 1st `  s
) )  /  h ]_ [_ ( 2nd `  s
)  /  a ]_ <. ( ( 1st `  ( 1st `  s ) )  i^i  [_ U. ( (mVars `  t ) " (
h  u.  { a } ) )  / 
z ]_ ( z  X.  z ) ) ,  h ,  a >.
) )
Colors of variables: wff setvar class
This definition is referenced by:  msrfval  30004
  Copyright terms: Public domain W3C validator