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 32814
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 32794 . 2 class mPreSt
2 vt . . 3 setvar 𝑡
3 cvv 3469 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1537 . . . . . . . 8 class 𝑑
65ccnv 5531 . . . . . . 7 class 𝑑
76, 5wceq 1538 . . . . . 6 wff 𝑑 = 𝑑
82cv 1537 . . . . . . . 8 class 𝑡
9 cmdv 32789 . . . . . . . 8 class mDV
108, 9cfv 6334 . . . . . . 7 class (mDV‘𝑡)
1110cpw 4511 . . . . . 6 class 𝒫 (mDV‘𝑡)
127, 4, 11crab 3134 . . . . 5 class {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑}
13 cmex 32788 . . . . . . . 8 class mEx
148, 13cfv 6334 . . . . . . 7 class (mEx‘𝑡)
1514cpw 4511 . . . . . 6 class 𝒫 (mEx‘𝑡)
16 cfn 8496 . . . . . 6 class Fin
1715, 16cin 3907 . . . . 5 class (𝒫 (mEx‘𝑡) ∩ Fin)
1812, 17cxp 5530 . . . 4 class ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin))
1918, 14cxp 5530 . . 3 class (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))
202, 3, 19cmpt 5122 . 2 class (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
211, 20wceq 1538 1 wff mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
Colors of variables: wff setvar class
This definition is referenced by:  mpstval  32856
  Copyright terms: Public domain W3C validator