Metamath Proof Explorer

Definition df-mpst

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

Ref Expression
Assertion df-mpst ⊢ mPreSt = t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t | d -1 = d × 𝒫 mEx ⁡ t ∩ Fin × mEx ⁡ t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpst class mPreSt
1 vt setvar t
2 cvv class V
3 vd setvar d
4 cmdv class mDV
5 1 cv setvar t
6 5 4 cfv class mDV ⁡ t
7 6 cpw class 𝒫 mDV ⁡ t
8 3 cv setvar d
9 8 ccnv class d -1
10 9 8 wceq wff d -1 = d
11 10 3 7 crab class d ∈ 𝒫 mDV ⁡ t | d -1 = d
12 cmex class mEx
13 5 12 cfv class mEx ⁡ t
14 13 cpw class 𝒫 mEx ⁡ t
15 cfn class Fin
16 14 15 cin class 𝒫 mEx ⁡ t ∩ Fin
17 11 16 cxp class d ∈ 𝒫 mDV ⁡ t | d -1 = d × 𝒫 mEx ⁡ t ∩ Fin
18 17 13 cxp class d ∈ 𝒫 mDV ⁡ t | d -1 = d × 𝒫 mEx ⁡ t ∩ Fin × mEx ⁡ t
19 1 2 18 cmpt class t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t | d -1 = d × 𝒫 mEx ⁡ t ∩ Fin × mEx ⁡ t
20 0 19 wceq wff mPreSt = t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t | d -1 = d × 𝒫 mEx ⁡ t ∩ Fin × mEx ⁡ t