Theorem mthmsta

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

	Ref	Expression
Hypotheses	mthmsta.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
	mthmsta.s	⊢ 𝑆 = ( mPreSt ‘ 𝑇 )
Assertion	mthmsta	⊢ 𝑈 ⊆ 𝑆

Proof

Step	Hyp	Ref	Expression
1		mthmsta.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
2		mthmsta.s	⊢ 𝑆 = ( mPreSt ‘ 𝑇 )
3		eqid	⊢ ( mStRed ‘ 𝑇 ) = ( mStRed ‘ 𝑇 )
4		eqid	⊢ ( mPPSt ‘ 𝑇 ) = ( mPPSt ‘ 𝑇 )
5	3 4 1	mthmval	⊢ 𝑈 = ( ◡ ( mStRed ‘ 𝑇 ) “ ( ( mStRed ‘ 𝑇 ) “ ( mPPSt ‘ 𝑇 ) ) )
6		cnvimass	⊢ ( ◡ ( mStRed ‘ 𝑇 ) “ ( ( mStRed ‘ 𝑇 ) “ ( mPPSt ‘ 𝑇 ) ) ) ⊆ dom ( mStRed ‘ 𝑇 )
7	2 3	msrf	⊢ ( mStRed ‘ 𝑇 ) : 𝑆 ⟶ 𝑆
8	7	fdmi	⊢ dom ( mStRed ‘ 𝑇 ) = 𝑆
9	6 8	sseqtri	⊢ ( ◡ ( mStRed ‘ 𝑇 ) “ ( ( mStRed ‘ 𝑇 ) “ ( mPPSt ‘ 𝑇 ) ) ) ⊆ 𝑆
10	5 9	eqsstri	⊢ 𝑈 ⊆ 𝑆