Definition df-mpst 35498

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 35478	. 2 class mPreSt
2		vt	. . 3 setvar 𝑡
3		cvv 3480	. . 3 class V
4		vd	. . . . . . . . 9 setvar 𝑑
5	4	cv 1539	. . . . . . . 8 class 𝑑
6	5	ccnv 5684	. . . . . . 7 class ◡𝑑
7	6, 5	wceq 1540	. . . . . 6 wff ◡𝑑 = 𝑑
8	2	cv 1539	. . . . . . . 8 class 𝑡
9		cmdv 35473	. . . . . . . 8 class mDV
10	8, 9	cfv 6561	. . . . . . 7 class (mDV‘𝑡)
11	10	cpw 4600	. . . . . 6 class 𝒫 (mDV‘𝑡)
12	7, 4, 11	crab 3436	. . . . 5 class {𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑}
13		cmex 35472	. . . . . . . 8 class mEx
14	8, 13	cfv 6561	. . . . . . 7 class (mEx‘𝑡)
15	14	cpw 4600	. . . . . 6 class 𝒫 (mEx‘𝑡)
16		cfn 8985	. . . . . 6 class Fin
17	15, 16	cin 3950	. . . . 5 class (𝒫 (mEx‘𝑡) ∩ Fin)
18	12, 17	cxp 5683	. . . 4 class ({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin))
19	18, 14	cxp 5683	. . 3 class (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡))
20	2, 3, 19	cmpt 5225	. 2 class (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))
21	1, 20	wceq 1540	1 wff mPreSt = (𝑡 ∈ V ↦ (({𝑑 ∈ 𝒫 (mDV‘𝑡) ∣ ◡𝑑 = 𝑑} × (𝒫 (mEx‘𝑡) ∩ Fin)) × (mEx‘𝑡)))

This definition is referenced by:  mpstval  35540