Theorem mppspst

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

	Ref	Expression
Hypotheses	mppsval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	mppsval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
Assertion	mppspst	⊢ 𝐽 ⊆ 𝑃

Proof

Step	Hyp	Ref	Expression
1		mppsval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		mppsval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
3		eqid	⊢ ( mCls ‘ 𝑇 ) = ( mCls ‘ 𝑇 )
4	1 2 3	mppsval	⊢ 𝐽 = { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑇 ) ℎ ) ) }
5	1 2 3	mppspstlem	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑇 ) ℎ ) ) } ⊆ 𝑃
6	4 5	eqsstri	⊢ 𝐽 ⊆ 𝑃