Theorem mppspst

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

	Ref	Expression
Hypotheses	mppsval.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
	mppsval.j	$$⊢J=\mathrm{mPPSt}\left(T\right)$$
Assertion	mppspst	$$⊢J\subseteq P$$

Proof

Step	Hyp	Ref	Expression
1		mppsval.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
2		mppsval.j	$$⊢J=\mathrm{mPPSt}\left(T\right)$$
3		eqid	$$⊢\mathrm{mCls}\left(T\right)=\mathrm{mCls}\left(T\right)$$
4	1 2 3	mppsval	$$⊢J=\left\{⟨⟨d,h⟩,a⟩|\left(⟨d,h,a⟩\in P\wedge a\in \left(d\mathrm{mCls}\left(T\right)h\right)\right)\right\}$$
5	1 2 3	mppspstlem	$$⊢\left\{⟨⟨d,h⟩,a⟩|\left(⟨d,h,a⟩\in P\wedge a\in \left(d\mathrm{mCls}\left(T\right)h\right)\right)\right\}\subseteq P$$
6	4 5	eqsstri	$$⊢J\subseteq P$$