Theorem mstapst

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

	Ref	Expression
Hypotheses	mstapst.p	|- P = ( mPreSt ` T )
	mstapst.s	|- S = ( mStat ` T )
Assertion	mstapst	|- S C_ P

Proof

Step	Hyp	Ref	Expression
1		mstapst.p	|- P = ( mPreSt ` T )
2		mstapst.s	|- S = ( mStat ` T )
3		eqid	|- ( mStRed ` T ) = ( mStRed ` T )
4	3 2	mstaval	|- S = ran ( mStRed ` T )
5	1 3	msrf	|- ( mStRed ` T ) : P --> P
6		frn	|- ( ( mStRed ` T ) : P --> P -> ran ( mStRed ` T ) C_ P )
7	5 6	ax-mp	|- ran ( mStRed ` T ) C_ P
8	4 7	eqsstri	|- S C_ P