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 33452
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 33432 . 2 class mPreSt
2 vt . . 3 setvar 𝑡
3 cvv 3431 . . 3 class V
4 vd . . . . . . . . 9 setvar 𝑑
54cv 1538 . . . . . . . 8 class 𝑑
65ccnv 5590 . . . . . . 7 class 𝑑
76, 5wceq 1539 . . . . . 6 wff 𝑑 = 𝑑
82cv 1538 . . . . . . . 8 class 𝑡
9 cmdv 33427 . . . . . . . 8 class mDV
108, 9cfv 6435 . . . . . . 7 class (mDV‘𝑡)
1110cpw 4535 . . . . . 6 class 𝒫 (mDV‘𝑡)
127, 4, 11crab 3068 . . . . 5 class {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑}
13 cmex 33426 . . . . . . . 8 class mEx
148, 13cfv 6435 . . . . . . 7 class (mEx‘𝑡)
1514cpw 4535 . . . . . 6 class 𝒫 (mEx‘𝑡)
16 cfn 8731 . . . . . 6 class Fin
1715, 16cin 3887 . . . . 5 class (𝒫 (mEx‘𝑡) ∩ Fin)
1812, 17cxp 5589 . . . 4 class ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin))
1918, 14cxp 5589 . . 3 class (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))
202, 3, 19cmpt 5159 . 2 class (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
211, 20wceq 1539 1 wff mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ 𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
Colors of variables: wff setvar class
This definition is referenced by:  mpstval  33494
  Copyright terms: Public domain W3C validator