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

Definition df-mpps 30144
Description: Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mpps  |- mPPSt  =  ( t  e.  _V  |->  {
<. <. d ,  h >. ,  a >.  |  (
<. d ,  h ,  a >.  e.  (mPreSt `  t )  /\  a  e.  ( d (mCls `  t ) h ) ) } )
Distinct variable group:    a, d, h, t

Detailed syntax breakdown of Definition df-mpps
StepHypRef Expression
1 cmpps 30124 . 2  class mPPSt
2 vt . . 3  setvar  t
3 cvv 3080 . . 3  class  _V
4 vd . . . . . . . 8  setvar  d
54cv 1436 . . . . . . 7  class  d
6 vh . . . . . . . 8  setvar  h
76cv 1436 . . . . . . 7  class  h
8 va . . . . . . . 8  setvar  a
98cv 1436 . . . . . . 7  class  a
105, 7, 9cotp 4006 . . . . . 6  class  <. d ,  h ,  a >.
112cv 1436 . . . . . . 7  class  t
12 cmpst 30119 . . . . . . 7  class mPreSt
1311, 12cfv 5601 . . . . . 6  class  (mPreSt `  t )
1410, 13wcel 1872 . . . . 5  wff  <. d ,  h ,  a >.  e.  (mPreSt `  t )
15 cmcls 30123 . . . . . . . 8  class mCls
1611, 15cfv 5601 . . . . . . 7  class  (mCls `  t )
175, 7, 16co 6305 . . . . . 6  class  ( d (mCls `  t )
h )
189, 17wcel 1872 . . . . 5  wff  a  e.  ( d (mCls `  t ) h )
1914, 18wa 370 . . . 4  wff  ( <.
d ,  h ,  a >.  e.  (mPreSt `  t )  /\  a  e.  ( d (mCls `  t ) h ) )
2019, 4, 6, 8coprab 6306 . . 3  class  { <. <.
d ,  h >. ,  a >.  |  ( <. d ,  h ,  a >.  e.  (mPreSt `  t )  /\  a  e.  ( d (mCls `  t ) h ) ) }
212, 3, 20cmpt 4482 . 2  class  ( t  e.  _V  |->  { <. <.
d ,  h >. ,  a >.  |  ( <. d ,  h ,  a >.  e.  (mPreSt `  t )  /\  a  e.  ( d (mCls `  t ) h ) ) } )
221, 21wceq 1437 1  wff mPPSt  =  ( t  e.  _V  |->  {
<. <. d ,  h >. ,  a >.  |  (
<. d ,  h ,  a >.  e.  (mPreSt `  t )  /\  a  e.  ( d (mCls `  t ) h ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  mppsval  30218
  Copyright terms: Public domain W3C validator