Theorem mthmsta

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

	Ref	Expression
Hypotheses	mthmsta.u	|- U = ( mThm ` T )
	mthmsta.s	|- S = ( mPreSt ` T )
Assertion	mthmsta	|- U C_ S

Proof

Step	Hyp	Ref	Expression
1		mthmsta.u	|- U = ( mThm ` T )
2		mthmsta.s	|- S = ( mPreSt ` T )
3		eqid	|- ( mStRed ` T ) = ( mStRed ` T )
4		eqid	|- ( mPPSt ` T ) = ( mPPSt ` T )
5	3 4 1	mthmval	|- U = ( `' ( mStRed ` T ) " ( ( mStRed ` T ) " ( mPPSt ` T ) ) )
6		cnvimass	|- ( `' ( mStRed ` T ) " ( ( mStRed ` T ) " ( mPPSt ` T ) ) ) C_ dom ( mStRed ` T )
7	2 3	msrf	|- ( mStRed ` T ) : S --> S
8	7	fdmi	|- dom ( mStRed ` T ) = S
9	6 8	sseqtri	|- ( `' ( mStRed ` T ) " ( ( mStRed ` T ) " ( mPPSt ` T ) ) ) C_ S
10	5 9	eqsstri	|- U C_ S