Theorem mthmsta

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

	Ref	Expression
Hypotheses	mthmsta.u	$$⊢U=\mathrm{mThm}\left(T\right)$$
	mthmsta.s	$$⊢S=\mathrm{mPreSt}\left(T\right)$$
Assertion	mthmsta	$$⊢U\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		mthmsta.u	$$⊢U=\mathrm{mThm}\left(T\right)$$
2		mthmsta.s	$$⊢S=\mathrm{mPreSt}\left(T\right)$$
3		eqid	$$⊢\mathrm{mStRed}\left(T\right)=\mathrm{mStRed}\left(T\right)$$
4		eqid	$$⊢\mathrm{mPPSt}\left(T\right)=\mathrm{mPPSt}\left(T\right)$$
5	3 4 1	mthmval	$$⊢U={\mathrm{mStRed}\left(T\right)}^{-1}\left[\mathrm{mStRed}\left(T\right)\left[\mathrm{mPPSt}\left(T\right)\right]\right]$$
6		cnvimass	$$⊢{\mathrm{mStRed}\left(T\right)}^{-1}\left[\mathrm{mStRed}\left(T\right)\left[\mathrm{mPPSt}\left(T\right)\right]\right]\subseteq \mathrm{dom}\mathrm{mStRed}\left(T\right)$$
7	2 3	msrf	$$⊢\mathrm{mStRed}\left(T\right):S⟶S$$
8	7	fdmi	$$⊢\mathrm{dom}\mathrm{mStRed}\left(T\right)=S$$
9	6 8	sseqtri	$$⊢{\mathrm{mStRed}\left(T\right)}^{-1}\left[\mathrm{mStRed}\left(T\right)\left[\mathrm{mPPSt}\left(T\right)\right]\right]\subseteq S$$
10	5 9	eqsstri	$$⊢U\subseteq S$$