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 31668
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 31648 . 2 class mPreSt
2 vt . . 3 setvar 𝑡
3 cvv 3328 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1619 . . . . . . . 8 class 𝑑
65ccnv 5253 . . . . . . 7 class 𝑑
76, 5wceq 1620 . . . . . 6 wff 𝑑 = 𝑑
82cv 1619 . . . . . . . 8 class 𝑡
9 cmdv 31643 . . . . . . . 8 class mDV
108, 9cfv 6037 . . . . . . 7 class (mDV‘𝑡)
1110cpw 4290 . . . . . 6 class 𝒫 (mDV‘𝑡)
127, 4, 11crab 3042 . . . . 5 class {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑}
13 cmex 31642 . . . . . . . 8 class mEx
148, 13cfv 6037 . . . . . . 7 class (mEx‘𝑡)
1514cpw 4290 . . . . . 6 class 𝒫 (mEx‘𝑡)
16 cfn 8109 . . . . . 6 class Fin
1715, 16cin 3702 . . . . 5 class (𝒫 (mEx‘𝑡) ∩ Fin)
1812, 17cxp 5252 . . . 4 class ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin))
1918, 14cxp 5252 . . 3 class (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))
202, 3, 19cmpt 4869 . 2 class (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
211, 20wceq 1620 1 wff mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
Colors of variables: wff setvar class
This definition is referenced by:  mpstval  31710
  Copyright terms: Public domain W3C validator