mppspstlem

	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⟩ \in P \land a \in (d C h))\} \subseteq P$

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⟩ \in P \land a \in (d C h))\} = \{x \| \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h)))\}$
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 (x \in P \leftrightarrow ⟨d, h, a⟩ \in P)$
9	8	biimpar	$⊢ (x = ⟨⟨d, h⟩, a⟩ \land ⟨d, h, a⟩ \in P) \to x \in P$
10	9	adantrr	$⊢ (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h))) \to x \in P$
11	10	exlimiv	$⊢ \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h))) \to x \in P$
12	11	exlimivv	$⊢ \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h))) \to x \in P$
13	12	abssi	$⊢ \{x \| \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h)))\} \subseteq P$
14	4 13	eqsstri	$⊢ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \subseteq P$

Metamath Proof Explorer