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	$⊢ P = mPreSt (T)$
	mppsval.j	$⊢ J = mPPSt (T)$
	mppsval.c	$⊢ C = mCls (T)$
Assertion	elmpps	$⊢ ⟨D, H, A⟩ \in J \leftrightarrow (⟨D, H, A⟩ \in P \land A \in (D C H))$

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-ot	$⊢ ⟨D, H, A⟩ = ⟨⟨D, H⟩, A⟩$
5	1 2 3	mppsval	$⊢ J = \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\}$
6	4 5	eleq12i	$⊢ ⟨D, H, A⟩ \in J \leftrightarrow ⟨⟨D, H⟩, A⟩ \in \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\}$
7		oprabss	$⊢ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \subseteq (V \times V) \times V$
8	7	sseli	$⊢ ⟨⟨D, H⟩, A⟩ \in \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \to ⟨⟨D, H⟩, A⟩ \in ((V \times V) \times V)$
9	1	mpstssv	$⊢ P \subseteq (V \times V) \times V$
10	9	sseli	$⊢ ⟨D, H, A⟩ \in P \to ⟨D, H, A⟩ \in ((V \times V) \times V)$
11	4 10	eqeltrrid	$⊢ ⟨D, H, A⟩ \in P \to ⟨⟨D, H⟩, A⟩ \in ((V \times V) \times V)$
12	11	adantr	$⊢ (⟨D, H, A⟩ \in P \land A \in (D C H)) \to ⟨⟨D, H⟩, A⟩ \in ((V \times V) \times V)$
13		opelxp	$⊢ ⟨⟨D, H⟩, A⟩ \in ((V \times V) \times V) \leftrightarrow (⟨D, H⟩ \in (V \times V) \land A \in V)$
14		opelxp	$⊢ ⟨D, H⟩ \in (V \times V) \leftrightarrow (D \in V \land H \in V)$
15		simp1	$⊢ (d = D \land h = H \land a = A) \to d = D$
16		simp2	$⊢ (d = D \land h = H \land a = A) \to h = H$
17		simp3	$⊢ (d = D \land h = H \land a = A) \to a = A$
18	15 16 17	oteq123d	$⊢ (d = D \land h = H \land a = A) \to ⟨d, h, a⟩ = ⟨D, H, A⟩$
19	18	eleq1d	$⊢ (d = D \land h = H \land a = A) \to (⟨d, h, a⟩ \in P \leftrightarrow ⟨D, H, A⟩ \in P)$
20	15 16	oveq12d	$⊢ (d = D \land h = H \land a = A) \to d C h = D C H$
21	17 20	eleq12d	$⊢ (d = D \land h = H \land a = A) \to (a \in (d C h) \leftrightarrow A \in (D C H))$
22	19 21	anbi12d	$⊢ (d = D \land h = H \land a = A) \to ((⟨d, h, a⟩ \in P \land a \in (d C h)) \leftrightarrow (⟨D, H, A⟩ \in P \land A \in (D C H)))$
23	22	eloprabga	$⊢ (D \in V \land H \in V \land A \in V) \to (⟨⟨D, H⟩, A⟩ \in \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \leftrightarrow (⟨D, H, A⟩ \in P \land A \in (D C H)))$
24	23	3expa	$⊢ ((D \in V \land H \in V) \land A \in V) \to (⟨⟨D, H⟩, A⟩ \in \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \leftrightarrow (⟨D, H, A⟩ \in P \land A \in (D C H)))$
25	14 24	sylanb	$⊢ (⟨D, H⟩ \in (V \times V) \land A \in V) \to (⟨⟨D, H⟩, A⟩ \in \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \leftrightarrow (⟨D, H, A⟩ \in P \land A \in (D C H)))$
26	13 25	sylbi	$⊢ ⟨⟨D, H⟩, A⟩ \in ((V \times V) \times V) \to (⟨⟨D, H⟩, A⟩ \in \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \leftrightarrow (⟨D, H, A⟩ \in P \land A \in (D C H)))$
27	8 12 26	pm5.21nii	$⊢ ⟨⟨D, H⟩, A⟩ \in \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \leftrightarrow (⟨D, H, A⟩ \in P \land A \in (D C H))$
28	6 27	bitri	$⊢ ⟨D, H, A⟩ \in J \leftrightarrow (⟨D, H, A⟩ \in P \land A \in (D C H))$

Metamath Proof Explorer

Theorem elmpps

Proof