Theorem mstapst

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

	Ref	Expression
Hypotheses	mstapst.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
	mstapst.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
Assertion	mstapst	$$⊢S\subseteq P$$

Proof

Step	Hyp	Ref	Expression
1		mstapst.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
2		mstapst.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
3		eqid	$$⊢\mathrm{mStRed}\left(T\right)=\mathrm{mStRed}\left(T\right)$$
4	3 2	mstaval	$$⊢S=\mathrm{ran}\mathrm{mStRed}\left(T\right)$$
5	1 3	msrf	$$⊢\mathrm{mStRed}\left(T\right):P⟶P$$
6		frn	$$⊢\mathrm{mStRed}\left(T\right):P⟶P\to \mathrm{ran}\mathrm{mStRed}\left(T\right)\subseteq P$$
7	5 6	ax-mp	$$⊢\mathrm{ran}\mathrm{mStRed}\left(T\right)\subseteq P$$
8	4 7	eqsstri	$$⊢S\subseteq P$$