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 31364
 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 31344 . 2 class mPreSt
2 vt . . 3 setvar 𝑡
3 cvv 3195 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1480 . . . . . . . 8 class 𝑑
65ccnv 5103 . . . . . . 7 class 𝑑
76, 5wceq 1481 . . . . . 6 wff 𝑑 = 𝑑
82cv 1480 . . . . . . . 8 class 𝑡
9 cmdv 31339 . . . . . . . 8 class mDV
108, 9cfv 5876 . . . . . . 7 class (mDV‘𝑡)
1110cpw 4149 . . . . . 6 class 𝒫 (mDV‘𝑡)
127, 4, 11crab 2913 . . . . 5 class {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑}
13 cmex 31338 . . . . . . . 8 class mEx
148, 13cfv 5876 . . . . . . 7 class (mEx‘𝑡)
1514cpw 4149 . . . . . 6 class 𝒫 (mEx‘𝑡)
16 cfn 7940 . . . . . 6 class Fin
1715, 16cin 3566 . . . . 5 class (𝒫 (mEx‘𝑡) ∩ Fin)
1812, 17cxp 5102 . . . 4 class ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin))
1918, 14cxp 5102 . . 3 class (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))
202, 3, 19cmpt 4720 . 2 class (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
211, 20wceq 1481 1 wff mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
 Colors of variables: wff setvar class This definition is referenced by:  mpstval  31406
 Copyright terms: Public domain W3C validator