Metamath Proof Explorer

Definition df-mpps

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

Ref Expression
Assertion df-mpps ⊢ mPPSt = t ∈ V ⟼ d h a | d h a ∈ mPreSt ⁡ t ∧ a ∈ d mCls ⁡ t h

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpps class mPPSt
1 vt setvar t
2 cvv class V
3 vd setvar d
4 vh setvar h
5 va setvar a
6 3 cv setvar d
7 4 cv setvar h
8 5 cv setvar a
9 6 7 8 cotp class d h a
10 cmpst class mPreSt
11 1 cv setvar t
12 11 10 cfv class mPreSt ⁡ t
13 9 12 wcel wff d h a ∈ mPreSt ⁡ t
14 cmcls class mCls
15 11 14 cfv class mCls ⁡ t
16 6 7 15 co class d mCls ⁡ t h
17 8 16 wcel wff a ∈ d mCls ⁡ t h
18 13 17 wa wff d h a ∈ mPreSt ⁡ t ∧ a ∈ d mCls ⁡ t h
19 18 3 4 5 coprab class d h a | d h a ∈ mPreSt ⁡ t ∧ a ∈ d mCls ⁡ t h
20 1 2 19 cmpt class t ∈ V ⟼ d h a | d h a ∈ mPreSt ⁡ t ∧ a ∈ d mCls ⁡ t h
21 0 20 wceq wff mPPSt = t ∈ V ⟼ d h a | d h a ∈ mPreSt ⁡ t ∧ a ∈ d mCls ⁡ t h