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

Definition df-mpps 34156
Description: Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mpps mPPSt = (𝑑 ∈ V ↦ {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))})
Distinct variable group:   π‘Ž,𝑑,β„Ž,𝑑

Detailed syntax breakdown of Definition df-mpps
StepHypRef Expression
1 cmpps 34136 . 2 class mPPSt
2 vt . . 3 setvar 𝑑
3 cvv 3447 . . 3 class V
4 vd . . . . . . . 8 setvar 𝑑
54cv 1541 . . . . . . 7 class 𝑑
6 vh . . . . . . . 8 setvar β„Ž
76cv 1541 . . . . . . 7 class β„Ž
8 va . . . . . . . 8 setvar π‘Ž
98cv 1541 . . . . . . 7 class π‘Ž
105, 7, 9cotp 4598 . . . . . 6 class βŸ¨π‘‘, β„Ž, π‘ŽβŸ©
112cv 1541 . . . . . . 7 class 𝑑
12 cmpst 34131 . . . . . . 7 class mPreSt
1311, 12cfv 6500 . . . . . 6 class (mPreStβ€˜π‘‘)
1410, 13wcel 2107 . . . . 5 wff βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘)
15 cmcls 34135 . . . . . . . 8 class mCls
1611, 15cfv 6500 . . . . . . 7 class (mClsβ€˜π‘‘)
175, 7, 16co 7361 . . . . . 6 class (𝑑(mClsβ€˜π‘‘)β„Ž)
189, 17wcel 2107 . . . . 5 wff π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž)
1914, 18wa 397 . . . 4 wff (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))
2019, 4, 6, 8coprab 7362 . . 3 class {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))}
212, 3, 20cmpt 5192 . 2 class (𝑑 ∈ V ↦ {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))})
221, 21wceq 1542 1 wff mPPSt = (𝑑 ∈ V ↦ {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))})
Colors of variables: wff setvar class
This definition is referenced by:  mppsval  34230
  Copyright terms: Public domain W3C validator