Theorem mpstssv

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

	Ref	Expression
Hypothesis	mpstssv.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
Assertion	mpstssv	$$⊢P\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		mpstssv.p	$$⊢P=\mathrm{mPreSt}\left(T\right)$$
2		eqid	$$⊢\mathrm{mDV}\left(T\right)=\mathrm{mDV}\left(T\right)$$
3		eqid	$$⊢\mathrm{mEx}\left(T\right)=\mathrm{mEx}\left(T\right)$$
4	2 3 1	mpstval	$$⊢P=\left(\left\{d\in 𝒫\mathrm{mDV}\left(T\right)|d^{-1}=d\right\}\times \left(𝒫\mathrm{mEx}\left(T\right)\cap \mathrm{Fin}\right)\right)\times \mathrm{mEx}\left(T\right)$$
5		xpss	$$⊢\left\{d\in 𝒫\mathrm{mDV}\left(T\right)|d^{-1}=d\right\}\times \left(𝒫\mathrm{mEx}\left(T\right)\cap \mathrm{Fin}\right)\subseteq \mathrm{V}\times \mathrm{V}$$
6		ssv	$$⊢\mathrm{mEx}\left(T\right)\subseteq \mathrm{V}$$
7		xpss12	$$⊢\left(\left\{d\in 𝒫\mathrm{mDV}\left(T\right)|d^{-1}=d\right\}\times \left(𝒫\mathrm{mEx}\left(T\right)\cap \mathrm{Fin}\right)\subseteq \mathrm{V}\times \mathrm{V}\wedge \mathrm{mEx}\left(T\right)\subseteq \mathrm{V}\right)\to \left(\left\{d\in 𝒫\mathrm{mDV}\left(T\right)|d^{-1}=d\right\}\times \left(𝒫\mathrm{mEx}\left(T\right)\cap \mathrm{Fin}\right)\right)\times \mathrm{mEx}\left(T\right)\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}$$
8	5 6 7	mp2an	$$⊢\left(\left\{d\in 𝒫\mathrm{mDV}\left(T\right)|d^{-1}=d\right\}\times \left(𝒫\mathrm{mEx}\left(T\right)\cap \mathrm{Fin}\right)\right)\times \mathrm{mEx}\left(T\right)\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}$$
9	4 8	eqsstri	$$⊢P\subseteq \left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}$$