Theorem elmpps

Description: Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mppsval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	mppsval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
	mppsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
Assertion	elmpps	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mppsval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		mppsval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
3		mppsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
4		df-ot	⊢ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ = ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩
5	1 2 3	mppsval	⊢ 𝐽 = { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) }
6	4 5	eleq12i	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ↔ ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } )
7		oprabss	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ⊆ ( ( V × V ) × V )
8	7	sseli	⊢ ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } → ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( V × V ) × V ) )
9	1	mpstssv	⊢ 𝑃 ⊆ ( ( V × V ) × V )
10	9	sseli	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ ( ( V × V ) × V ) )
11	4 10	eqeltrrid	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( V × V ) × V ) )
12	11	adantr	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) → ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( V × V ) × V ) )
13		opelxp	⊢ ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( V × V ) × V ) ↔ ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( V × V ) ∧ 𝐴 ∈ V ) )
14		opelxp	⊢ ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( V × V ) ↔ ( 𝐷 ∈ V ∧ 𝐻 ∈ V ) )
15		simp1	⊢ ( ( 𝑑 = 𝐷 ∧ ℎ = 𝐻 ∧ 𝑎 = 𝐴 ) → 𝑑 = 𝐷 )
16		simp2	⊢ ( ( 𝑑 = 𝐷 ∧ ℎ = 𝐻 ∧ 𝑎 = 𝐴 ) → ℎ = 𝐻 )
17		simp3	⊢ ( ( 𝑑 = 𝐷 ∧ ℎ = 𝐻 ∧ 𝑎 = 𝐴 ) → 𝑎 = 𝐴 )
18	15 16 17	oteq123d	⊢ ( ( 𝑑 = 𝐷 ∧ ℎ = 𝐻 ∧ 𝑎 = 𝐴 ) → ⟨ 𝑑 , ℎ , 𝑎 ⟩ = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ )
19	18	eleq1d	⊢ ( ( 𝑑 = 𝐷 ∧ ℎ = 𝐻 ∧ 𝑎 = 𝐴 ) → ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ↔ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ) )
20	15 16	oveq12d	⊢ ( ( 𝑑 = 𝐷 ∧ ℎ = 𝐻 ∧ 𝑎 = 𝐴 ) → ( 𝑑 𝐶 ℎ ) = ( 𝐷 𝐶 𝐻 ) )
21	17 20	eleq12d	⊢ ( ( 𝑑 = 𝐷 ∧ ℎ = 𝐻 ∧ 𝑎 = 𝐴 ) → ( 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ↔ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) )
22	19 21	anbi12d	⊢ ( ( 𝑑 = 𝐷 ∧ ℎ = 𝐻 ∧ 𝑎 = 𝐴 ) → ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) ) )
23	22	eloprabga	⊢ ( ( 𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) → ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) ) )
24	23	3expa	⊢ ( ( ( 𝐷 ∈ V ∧ 𝐻 ∈ V ) ∧ 𝐴 ∈ V ) → ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) ) )
25	14 24	sylanb	⊢ ( ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( V × V ) ∧ 𝐴 ∈ V ) → ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) ) )
26	13 25	sylbi	⊢ ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( V × V ) × V ) → ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) ) )
27	8 12 26	pm5.21nii	⊢ ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) )
28	6 27	bitri	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐴 ∈ ( 𝐷 𝐶 𝐻 ) ) )