Theorem mppspst

Description: A provable pre-statement is a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mppsval.p	|- P = ( mPreSt ` T )
	mppsval.j	|- J = ( mPPSt ` T )
Assertion	mppspst	|- J C_ P

Proof

Step	Hyp	Ref	Expression
1		mppsval.p	|- P = ( mPreSt ` T )
2		mppsval.j	|- J = ( mPPSt ` T )
3		eqid	|- ( mCls ` T ) = ( mCls ` T )
4	1 2 3	mppsval	|- J = { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d ( mCls ` T ) h ) ) }
5	1 2 3	mppspstlem	|- { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d ( mCls ` T ) h ) ) } C_ P
6	4 5	eqsstri	|- J C_ P