Theorem mppspstlem

Description: Lemma for mppspst . (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mppsval.p	|- P = ( mPreSt ` T )
	mppsval.j	|- J = ( mPPSt ` T )
	mppsval.c	|- C = ( mCls ` T )
Assertion	mppspstlem	|- { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } C_ P

Proof

Step	Hyp	Ref	Expression
1		mppsval.p	|- P = ( mPreSt ` T )
2		mppsval.j	|- J = ( mPPSt ` T )
3		mppsval.c	|- C = ( mCls ` T )
4		df-oprab	|- { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } = { x | E. d E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) }
5		df-ot	|- <. d , h , a >. = <. <. d , h >. , a >.
6	5	eqeq2i	|- ( x = <. d , h , a >. <-> x = <. <. d , h >. , a >. )
7	6	biimpri	|- ( x = <. <. d , h >. , a >. -> x = <. d , h , a >. )
8	7	eleq1d	|- ( x = <. <. d , h >. , a >. -> ( x e. P <-> <. d , h , a >. e. P ) )
9	8	biimpar	|- ( ( x = <. <. d , h >. , a >. /\ <. d , h , a >. e. P ) -> x e. P )
10	9	adantrr	|- ( ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) -> x e. P )
11	10	exlimiv	|- ( E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) -> x e. P )
12	11	exlimivv	|- ( E. d E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) -> x e. P )
13	12	abssi	|- { x | E. d E. h E. a ( x = <. <. d , h >. , a >. /\ ( <. d , h , a >. e. P /\ a e. ( d C h ) ) ) } C_ P
14	4 13	eqsstri	|- { <. <. d , h >. , a >. | ( <. d , h , a >. e. P /\ a e. ( d C h ) ) } C_ P