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 34484
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 34464 . 2 class mPPSt
2 vt . . 3 setvar 𝑑
3 cvv 3474 . . 3 class V
4 vd . . . . . . . 8 setvar 𝑑
54cv 1540 . . . . . . 7 class 𝑑
6 vh . . . . . . . 8 setvar β„Ž
76cv 1540 . . . . . . 7 class β„Ž
8 va . . . . . . . 8 setvar π‘Ž
98cv 1540 . . . . . . 7 class π‘Ž
105, 7, 9cotp 4636 . . . . . 6 class βŸ¨π‘‘, β„Ž, π‘ŽβŸ©
112cv 1540 . . . . . . 7 class 𝑑
12 cmpst 34459 . . . . . . 7 class mPreSt
1311, 12cfv 6543 . . . . . 6 class (mPreStβ€˜π‘‘)
1410, 13wcel 2106 . . . . 5 wff βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘)
15 cmcls 34463 . . . . . . . 8 class mCls
1611, 15cfv 6543 . . . . . . 7 class (mClsβ€˜π‘‘)
175, 7, 16co 7408 . . . . . 6 class (𝑑(mClsβ€˜π‘‘)β„Ž)
189, 17wcel 2106 . . . . 5 wff π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž)
1914, 18wa 396 . . . 4 wff (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))
2019, 4, 6, 8coprab 7409 . . 3 class {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))}
212, 3, 20cmpt 5231 . 2 class (𝑑 ∈ V ↦ {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))})
221, 21wceq 1541 1 wff mPPSt = (𝑑 ∈ V ↦ {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mPreStβ€˜π‘‘) ∧ π‘Ž ∈ (𝑑(mClsβ€˜π‘‘)β„Ž))})
Colors of variables: wff setvar class
This definition is referenced by:  mppsval  34558
  Copyright terms: Public domain W3C validator