Theorem mstapst

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

	Ref	Expression
Hypotheses	mstapst.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	mstapst.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
Assertion	mstapst	⊢ 𝑆 ⊆ 𝑃

Proof

Step	Hyp	Ref	Expression
1		mstapst.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		mstapst.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
3		eqid	⊢ ( mStRed ‘ 𝑇 ) = ( mStRed ‘ 𝑇 )
4	3 2	mstaval	⊢ 𝑆 = ran ( mStRed ‘ 𝑇 )
5	1 3	msrf	⊢ ( mStRed ‘ 𝑇 ) : 𝑃 ⟶ 𝑃
6		frn	⊢ ( ( mStRed ‘ 𝑇 ) : 𝑃 ⟶ 𝑃 → ran ( mStRed ‘ 𝑇 ) ⊆ 𝑃 )
7	5 6	ax-mp	⊢ ran ( mStRed ‘ 𝑇 ) ⊆ 𝑃
8	4 7	eqsstri	⊢ 𝑆 ⊆ 𝑃