mpst123

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

		Ref	Expression
	Hypothesis	mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	Assertion	mpst123	⊢ ( 𝑋 ∈ 𝑃 → 𝑋 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ 𝑋 ) ⟩ )

Step	Hyp	Ref	Expression
1		mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2	1	mpstssv	⊢ 𝑃 ⊆ ( ( V × V ) × V )
3	2	sseli	⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( ( V × V ) × V ) )
4		1st2nd2	⊢ ( 𝑋 ∈ ( ( V × V ) × V ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
5		xp1st	⊢ ( 𝑋 ∈ ( ( V × V ) × V ) → ( 1^st ‘ 𝑋 ) ∈ ( V × V ) )
6		1st2nd2	⊢ ( ( 1^st ‘ 𝑋 ) ∈ ( V × V ) → ( 1^st ‘ 𝑋 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) ⟩ )
7	5 6	syl	⊢ ( 𝑋 ∈ ( ( V × V ) × V ) → ( 1^st ‘ 𝑋 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) ⟩ )
8	7	opeq1d	⊢ ( 𝑋 ∈ ( ( V × V ) × V ) → ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) ⟩ , ( 2^nd ‘ 𝑋 ) ⟩ )
9	4 8	eqtrd	⊢ ( 𝑋 ∈ ( ( V × V ) × V ) → 𝑋 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) ⟩ , ( 2^nd ‘ 𝑋 ) ⟩ )
10		df-ot	⊢ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) ⟩ , ( 2^nd ‘ 𝑋 ) ⟩
11	9 10	eqtr4di	⊢ ( 𝑋 ∈ ( ( V × V ) × V ) → 𝑋 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ 𝑋 ) ⟩ )
12	3 11	syl	⊢ ( 𝑋 ∈ 𝑃 → 𝑋 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑋 ) ) , ( 2^nd ‘ 𝑋 ) ⟩ )

Metamath Proof Explorer