mpst123

Description: Decompose a pre-statement into a triple of values. (Contributed by Mario Carneiro, 18-Jul-2016)

		Ref	Expression
	Hypothesis	mpstssv.p	$⊢ P = mPreSt (T)$
	Assertion	mpst123	$⊢ X \in P \to X = ⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X)), 2^{nd} (X)⟩$

Step	Hyp	Ref	Expression
1		mpstssv.p	$⊢ P = mPreSt (T)$
2	1	mpstssv	$⊢ P \subseteq (V \times V) \times V$
3	2	sseli	$⊢ X \in P \to X \in ((V \times V) \times V)$
4		1st2nd2	$⊢ X \in ((V \times V) \times V) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
5		xp1st	$⊢ X \in ((V \times V) \times V) \to 1^{st} (X) \in (V \times V)$
6		1st2nd2	$⊢ 1^{st} (X) \in (V \times V) \to 1^{st} (X) = ⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X))⟩$
7	5 6	syl	$⊢ X \in ((V \times V) \times V) \to 1^{st} (X) = ⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X))⟩$
8	7	opeq1d	$⊢ X \in ((V \times V) \times V) \to ⟨1^{st} (X), 2^{nd} (X)⟩ = ⟨⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X))⟩, 2^{nd} (X)⟩$
9	4 8	eqtrd	$⊢ X \in ((V \times V) \times V) \to X = ⟨⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X))⟩, 2^{nd} (X)⟩$
10		df-ot	$⊢ ⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X)), 2^{nd} (X)⟩ = ⟨⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X))⟩, 2^{nd} (X)⟩$
11	9 10	eqtr4di	$⊢ X \in ((V \times V) \times V) \to X = ⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X)), 2^{nd} (X)⟩$
12	3 11	syl	$⊢ X \in P \to X = ⟨1^{st} (1^{st} (X)), 2^{nd} (1^{st} (X)), 2^{nd} (X)⟩$

Metamath Proof Explorer