Definition df-mpst 32853

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

Step	Hyp	Ref	Expression
1		cmpst 32833	. 2 class mPreSt
2		vt	. . 3 setvar 𝑡
3		cvv 3441	. . 3 class V
4		vd	. . . . . . . . 9 setvar 𝑑
5	4	cv 1537	. . . . . . . 8 class 𝑑
6	5	ccnv 5518	. . . . . . 7 class ◡𝑑
7	6, 5	wceq 1538	. . . . . 6 wff ◡𝑑 = 𝑑
8	2	cv 1537	. . . . . . . 8 class 𝑡
9		cmdv 32828	. . . . . . . 8 class mDV
10	8, 9	cfv 6324	. . . . . . 7 class (mDV‘𝑡)
11	10	cpw 4497	. . . . . 6 class 𝒫 (mDV‘𝑡)
12	7, 4, 11	crab 3110	. . . . 5 class {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑}
13		cmex 32827	. . . . . . . 8 class mEx
14	8, 13	cfv 6324	. . . . . . 7 class (mEx‘𝑡)
15	14	cpw 4497	. . . . . 6 class 𝒫 (mEx‘𝑡)
16		cfn 8492	. . . . . 6 class Fin
17	15, 16	cin 3880	. . . . 5 class (𝒫 (mEx‘𝑡) ∩ Fin)
18	12, 17	cxp 5517	. . . 4 class ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin))
19	18, 14	cxp 5517	. . 3 class (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))
20	2, 3, 19	cmpt 5110	. 2 class (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
21	1, 20	wceq 1538	1 wff mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))

This definition is referenced by:  mpstval  32895