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

Definition df-mpst 34151
Description: Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mpst mPreSt = (𝑑 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDVβ€˜π‘‘) ∣ ◑𝑑 = 𝑑} Γ— (𝒫 (mExβ€˜π‘‘) ∩ Fin)) Γ— (mExβ€˜π‘‘)))
Distinct variable group:   𝑑,𝑑

Detailed syntax breakdown of Definition df-mpst
StepHypRef Expression
1 cmpst 34131 . 2 class mPreSt
2 vt . . 3 setvar 𝑑
3 cvv 3447 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1541 . . . . . . . 8 class 𝑑
65ccnv 5636 . . . . . . 7 class ◑𝑑
76, 5wceq 1542 . . . . . 6 wff ◑𝑑 = 𝑑
82cv 1541 . . . . . . . 8 class 𝑑
9 cmdv 34126 . . . . . . . 8 class mDV
108, 9cfv 6500 . . . . . . 7 class (mDVβ€˜π‘‘)
1110cpw 4564 . . . . . 6 class 𝒫 (mDVβ€˜π‘‘)
127, 4, 11crab 3406 . . . . 5 class {𝑑 ∈ 𝒫 (mDVβ€˜π‘‘) ∣ ◑𝑑 = 𝑑}
13 cmex 34125 . . . . . . . 8 class mEx
148, 13cfv 6500 . . . . . . 7 class (mExβ€˜π‘‘)
1514cpw 4564 . . . . . 6 class 𝒫 (mExβ€˜π‘‘)
16 cfn 8889 . . . . . 6 class Fin
1715, 16cin 3913 . . . . 5 class (𝒫 (mExβ€˜π‘‘) ∩ Fin)
1812, 17cxp 5635 . . . 4 class ({𝑑 ∈ 𝒫 (mDVβ€˜π‘‘) ∣ ◑𝑑 = 𝑑} Γ— (𝒫 (mExβ€˜π‘‘) ∩ Fin))
1918, 14cxp 5635 . . 3 class (({𝑑 ∈ 𝒫 (mDVβ€˜π‘‘) ∣ ◑𝑑 = 𝑑} Γ— (𝒫 (mExβ€˜π‘‘) ∩ Fin)) Γ— (mExβ€˜π‘‘))
202, 3, 19cmpt 5192 . 2 class (𝑑 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDVβ€˜π‘‘) ∣ ◑𝑑 = 𝑑} Γ— (𝒫 (mExβ€˜π‘‘) ∩ Fin)) Γ— (mExβ€˜π‘‘)))
211, 20wceq 1542 1 wff mPreSt = (𝑑 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDVβ€˜π‘‘) ∣ ◑𝑑 = 𝑑} Γ— (𝒫 (mExβ€˜π‘‘) ∩ Fin)) Γ— (mExβ€˜π‘‘)))
Colors of variables: wff setvar class
This definition is referenced by:  mpstval  34193
  Copyright terms: Public domain W3C validator