Definition df-mpst

Description: Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mpst	⊢ mPreSt = ( 𝑡 ∈ V ↦ ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) ) × ( mEx ‘ 𝑡 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpst	⊢ mPreSt
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vd	⊢ 𝑑
4		cmdv	⊢ mDV
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mDV ‘ 𝑡 )
7	6	cpw	⊢ 𝒫 ( mDV ‘ 𝑡 )
8	3	cv	⊢ 𝑑
9	8	ccnv	⊢ ◡ 𝑑
10	9 8	wceq	⊢ ◡ 𝑑 = 𝑑
11	10 3 7	crab	⊢ { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 }
12		cmex	⊢ mEx
13	5 12	cfv	⊢ ( mEx ‘ 𝑡 )
14	13	cpw	⊢ 𝒫 ( mEx ‘ 𝑡 )
15		cfn	⊢ Fin
16	14 15	cin	⊢ ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin )
17	11 16	cxp	⊢ ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) )
18	17 13	cxp	⊢ ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) ) × ( mEx ‘ 𝑡 ) )
19	1 2 18	cmpt	⊢ ( 𝑡 ∈ V ↦ ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) ) × ( mEx ‘ 𝑡 ) ) )
20	0 19	wceq	⊢ mPreSt = ( 𝑡 ∈ V ↦ ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑡 ) ∩ Fin ) ) × ( mEx ‘ 𝑡 ) ) )