Theorem mpstssv

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

	Ref	Expression
Hypothesis	mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
Assertion	mpstssv	⊢ 𝑃 ⊆ ( ( V × V ) × V )

Proof

Step	Hyp	Ref	Expression
1		mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		eqid	⊢ ( mDV ‘ 𝑇 ) = ( mDV ‘ 𝑇 )
3		eqid	⊢ ( mEx ‘ 𝑇 ) = ( mEx ‘ 𝑇 )
4	2 3 1	mpstval	⊢ 𝑃 = ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑇 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑇 ) ∩ Fin ) ) × ( mEx ‘ 𝑇 ) )
5		xpss	⊢ ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑇 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑇 ) ∩ Fin ) ) ⊆ ( V × V )
6		ssv	⊢ ( mEx ‘ 𝑇 ) ⊆ V
7		xpss12	⊢ ( ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑇 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑇 ) ∩ Fin ) ) ⊆ ( V × V ) ∧ ( mEx ‘ 𝑇 ) ⊆ V ) → ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑇 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑇 ) ∩ Fin ) ) × ( mEx ‘ 𝑇 ) ) ⊆ ( ( V × V ) × V ) )
8	5 6 7	mp2an	⊢ ( ( { 𝑑 ∈ 𝒫 ( mDV ‘ 𝑇 ) ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 ( mEx ‘ 𝑇 ) ∩ Fin ) ) × ( mEx ‘ 𝑇 ) ) ⊆ ( ( V × V ) × V )
9	4 8	eqsstri	⊢ 𝑃 ⊆ ( ( V × V ) × V )