Definition df-mpps 31395

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

Assertion

Ref	Expression
df-mpps	|- mPPSt = ( t e. _V |-> { <. <. d , h >. , a >. | ( <. d , h , a >. e. (mPreSt ` t ) /\ a e. ( d (mCls ` t ) h ) ) } )

Distinct variable group:   a, d, h, t

Detailed syntax breakdown of Definition df-mpps

Step	Hyp	Ref	Expression
1		cmpps 31375	. 2 class mPPSt
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vd	. . . . . . . 8 setvar d
5	4	cv 1482	. . . . . . 7 class d
6		vh	. . . . . . . 8 setvar h
7	6	cv 1482	. . . . . . 7 class h
8		va	. . . . . . . 8 setvar a
9	8	cv 1482	. . . . . . 7 class a
10	5, 7, 9	cotp 4185	. . . . . 6 class <. d , h , a >.
11	2	cv 1482	. . . . . . 7 class t
12		cmpst 31370	. . . . . . 7 class mPreSt
13	11, 12	cfv 5888	. . . . . 6 class (mPreSt ` t )
14	10, 13	wcel 1990	. . . . 5 wff <. d , h , a >. e. (mPreSt ` t )
15		cmcls 31374	. . . . . . . 8 class mCls
16	11, 15	cfv 5888	. . . . . . 7 class (mCls ` t )
17	5, 7, 16	co 6650	. . . . . 6 class ( d (mCls ` t ) h )
18	9, 17	wcel 1990	. . . . 5 wff a e. ( d (mCls ` t ) h )
19	14, 18	wa 384	. . . 4 wff ( <. d , h , a >. e. (mPreSt ` t ) /\ a e. ( d (mCls ` t ) h ) )
20	19, 4, 6, 8	coprab 6651	. . 3 class { <. <. d , h >. , a >. | ( <. d , h , a >. e. (mPreSt ` t ) /\ a e. ( d (mCls ` t ) h ) ) }
21	2, 3, 20	cmpt 4729	. 2 class ( t e. _V |-> { <. <. d , h >. , a >. | ( <. d , h , a >. e. (mPreSt ` t ) /\ a e. ( d (mCls ` t ) h ) ) } )
22	1, 21	wceq 1483	1 wff mPPSt = ( t e. _V |-> { <. <. d , h >. , a >. | ( <. d , h , a >. e. (mPreSt ` t ) /\ a e. ( d (mCls ` t ) h ) ) } )

This definition is referenced by:  mppsval  31469