Theorem mppspstlem

Description: Lemma for mppspst . (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)$$
	mppsval.c	$$⊢C=\mathrm{mCls}\left(T\right)$$
Assertion	mppspstlem	$$⊢\left\{⟨⟨d,h⟩,a⟩|\left(⟨d,h,a⟩\in P\wedge a\in \left(dCh\right)\right)\right\}\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		mppsval.c	$$⊢C=\mathrm{mCls}\left(T\right)$$
4		df-oprab	$$⊢\left\{⟨⟨d,h⟩,a⟩|\left(⟨d,h,a⟩\in P\wedge a\in \left(dCh\right)\right)\right\}=\left\{x|\exists d\exists h\exists a\left(x=⟨⟨d,h⟩,a⟩\wedge \left(⟨d,h,a⟩\in P\wedge a\in \left(dCh\right)\right)\right)\right\}$$
5		df-ot	$$⊢⟨d,h,a⟩=⟨⟨d,h⟩,a⟩$$
6	5	eqeq2i	$$⊢x=⟨d,h,a⟩\leftrightarrow x=⟨⟨d,h⟩,a⟩$$
7	6	biimpri	$$⊢x=⟨⟨d,h⟩,a⟩\to x=⟨d,h,a⟩$$
8	7	eleq1d	$$⊢x=⟨⟨d,h⟩,a⟩\to \left(x\in P\leftrightarrow ⟨d,h,a⟩\in P\right)$$
9	8	biimpar	$$⊢\left(x=⟨⟨d,h⟩,a⟩\wedge ⟨d,h,a⟩\in P\right)\to x\in P$$
10	9	adantrr	$$⊢\left(x=⟨⟨d,h⟩,a⟩\wedge \left(⟨d,h,a⟩\in P\wedge a\in \left(dCh\right)\right)\right)\to x\in P$$
11	10	exlimiv	$$⊢\exists a\left(x=⟨⟨d,h⟩,a⟩\wedge \left(⟨d,h,a⟩\in P\wedge a\in \left(dCh\right)\right)\right)\to x\in P$$
12	11	exlimivv	$$⊢\exists d\exists h\exists a\left(x=⟨⟨d,h⟩,a⟩\wedge \left(⟨d,h,a⟩\in P\wedge a\in \left(dCh\right)\right)\right)\to x\in P$$
13	12	abssi	$$⊢\left\{x|\exists d\exists h\exists a\left(x=⟨⟨d,h⟩,a⟩\wedge \left(⟨d,h,a⟩\in P\wedge a\in \left(dCh\right)\right)\right)\right\}\subseteq P$$
14	4 13	eqsstri	$$⊢\left\{⟨⟨d,h⟩,a⟩|\left(⟨d,h,a⟩\in P\wedge a\in \left(dCh\right)\right)\right\}\subseteq P$$