Definition df-mpst 31390

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 31370	. 2 class mPreSt
2		vt	. . 3 setvar 𝑡
3		cvv 3200	. . 3 class V
4		vd	. . . . . . . . 9 setvar 𝑑
5	4	cv 1482	. . . . . . . 8 class 𝑑
6	5	ccnv 5113	. . . . . . 7 class ◡𝑑
7	6, 5	wceq 1483	. . . . . 6 wff ◡𝑑 = 𝑑
8	2	cv 1482	. . . . . . . 8 class 𝑡
9		cmdv 31365	. . . . . . . 8 class mDV
10	8, 9	cfv 5888	. . . . . . 7 class (mDV‘𝑡)
11	10	cpw 4158	. . . . . 6 class 𝒫 (mDV‘𝑡)
12	7, 4, 11	crab 2916	. . . . 5 class {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑}
13		cmex 31364	. . . . . . . 8 class mEx
14	8, 13	cfv 5888	. . . . . . 7 class (mEx‘𝑡)
15	14	cpw 4158	. . . . . 6 class 𝒫 (mEx‘𝑡)
16		cfn 7955	. . . . . 6 class Fin
17	15, 16	cin 3573	. . . . 5 class (𝒫 (mEx‘𝑡) ∩ Fin)
18	12, 17	cxp 5112	. . . 4 class ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin))
19	18, 14	cxp 5112	. . 3 class (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))
20	2, 3, 19	cmpt 4729	. 2 class (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
21	1, 20	wceq 1483	1 wff mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))

This definition is referenced by:  mpstval  31432