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