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

Definition df-mpst 29718
Description: Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mpst  |- mPreSt  =  ( t  e.  _V  |->  ( ( { d  e. 
~P (mDV `  t
)  |  `' d  =  d }  X.  ( ~P (mEx `  t
)  i^i  Fin )
)  X.  (mEx `  t ) ) )
Distinct variable group:    t, d

Detailed syntax breakdown of Definition df-mpst
StepHypRef Expression
1 cmpst 29698 . 2  class mPreSt
2 vt . . 3  setvar  t
3 cvv 3061 . . 3  class  _V
4 vd . . . . . . . . 9  setvar  d
54cv 1406 . . . . . . . 8  class  d
65ccnv 4824 . . . . . . 7  class  `' d
76, 5wceq 1407 . . . . . 6  wff  `' d  =  d
82cv 1406 . . . . . . . 8  class  t
9 cmdv 29693 . . . . . . . 8  class mDV
108, 9cfv 5571 . . . . . . 7  class  (mDV `  t )
1110cpw 3957 . . . . . 6  class  ~P (mDV `  t )
127, 4, 11crab 2760 . . . . 5  class  { d  e.  ~P (mDV `  t )  |  `' d  =  d }
13 cmex 29692 . . . . . . . 8  class mEx
148, 13cfv 5571 . . . . . . 7  class  (mEx `  t )
1514cpw 3957 . . . . . 6  class  ~P (mEx `  t )
16 cfn 7556 . . . . . 6  class  Fin
1715, 16cin 3415 . . . . 5  class  ( ~P (mEx `  t )  i^i  Fin )
1812, 17cxp 4823 . . . 4  class  ( { d  e.  ~P (mDV `  t )  |  `' d  =  d }  X.  ( ~P (mEx `  t )  i^i  Fin ) )
1918, 14cxp 4823 . . 3  class  ( ( { d  e.  ~P (mDV `  t )  |  `' d  =  d }  X.  ( ~P (mEx `  t )  i^i  Fin ) )  X.  (mEx `  t ) )
202, 3, 19cmpt 4455 . 2  class  ( t  e.  _V  |->  ( ( { d  e.  ~P (mDV `  t )  |  `' d  =  d }  X.  ( ~P (mEx `  t )  i^i  Fin ) )  X.  (mEx `  t ) ) )
211, 20wceq 1407 1  wff mPreSt  =  ( t  e.  _V  |->  ( ( { d  e. 
~P (mDV `  t
)  |  `' d  =  d }  X.  ( ~P (mEx `  t
)  i^i  Fin )
)  X.  (mEx `  t ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  mpstval  29760
  Copyright terms: Public domain W3C validator