Theorem mppspstlem

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

	Ref	Expression
Hypotheses	mppsval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	mppsval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
	mppsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
Assertion	mppspstlem	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ⊆ 𝑃

Proof

Step	Hyp	Ref	Expression
1		mppsval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		mppsval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
3		mppsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
4		df-oprab	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } = { 𝑥 ∣ ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) }
5		df-ot	⊢ ⟨ 𝑑 , ℎ , 𝑎 ⟩ = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩
6	5	eqeq2i	⊢ ( 𝑥 = ⟨ 𝑑 , ℎ , 𝑎 ⟩ ↔ 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ )
7	6	biimpri	⊢ ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ → 𝑥 = ⟨ 𝑑 , ℎ , 𝑎 ⟩ )
8	7	eleq1d	⊢ ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ → ( 𝑥 ∈ 𝑃 ↔ ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ) )
9	8	biimpar	⊢ ( ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ) → 𝑥 ∈ 𝑃 )
10	9	adantrr	⊢ ( ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) → 𝑥 ∈ 𝑃 )
11	10	exlimiv	⊢ ( ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) → 𝑥 ∈ 𝑃 )
12	11	exlimivv	⊢ ( ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) → 𝑥 ∈ 𝑃 )
13	12	abssi	⊢ { 𝑥 ∣ ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) } ⊆ 𝑃
14	4 13	eqsstri	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ⊆ 𝑃