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 e. _V |-> { <. <. d , h >. , a >. | ( <. d , h , a >. e. ( mPreSt ` t ) /\ a e. ( d ( mCls ` t ) h ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpps	|- mPPSt
1		vt	|- t
2		cvv	|- _V
3		vd	|- d
4		vh	|- h
5		va	|- a
6	3	cv	|- d
7	4	cv	|- h
8	5	cv	|- a
9	6 7 8	cotp	|- <. d , h , a >.
10		cmpst	|- mPreSt
11	1	cv	|- t
12	11 10	cfv	|- ( mPreSt ` t )
13	9 12	wcel	|- <. d , h , a >. e. ( mPreSt ` t )
14		cmcls	|- mCls
15	11 14	cfv	|- ( mCls ` t )
16	6 7 15	co	|- ( d ( mCls ` t ) h )
17	8 16	wcel	|- a e. ( d ( mCls ` t ) h )
18	13 17	wa	|- ( <. d , h , a >. e. ( mPreSt ` t ) /\ a e. ( d ( mCls ` t ) h ) )
19	18 3 4 5	coprab	|- { <. <. d , h >. , a >. | ( <. d , h , a >. e. ( mPreSt ` t ) /\ a e. ( d ( mCls ` t ) h ) ) }
20	1 2 19	cmpt	|- ( t e. _V |-> { <. <. d , h >. , a >. | ( <. d , h , a >. e. ( mPreSt ` t ) /\ a e. ( d ( mCls ` t ) h ) ) } )
21	0 20	wceq	|- mPPSt = ( t e. _V |-> { <. <. d , h >. , a >. | ( <. d , h , a >. e. ( mPreSt ` t ) /\ a e. ( d ( mCls ` t ) h ) ) } )