Metamath Proof Explorer


Theorem 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 ( 𝑋𝑃𝑋 = ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) , ( 2nd𝑋 ) ⟩ )

Proof

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 ) → 𝑋 = ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ )
5 xp1st ( 𝑋 ∈ ( ( V × V ) × V ) → ( 1st𝑋 ) ∈ ( V × V ) )
6 1st2nd2 ( ( 1st𝑋 ) ∈ ( V × V ) → ( 1st𝑋 ) = ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) ⟩ )
7 5 6 syl ( 𝑋 ∈ ( ( V × V ) × V ) → ( 1st𝑋 ) = ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) ⟩ )
8 7 opeq1d ( 𝑋 ∈ ( ( V × V ) × V ) → ⟨ ( 1st𝑋 ) , ( 2nd𝑋 ) ⟩ = ⟨ ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) ⟩ , ( 2nd𝑋 ) ⟩ )
9 4 8 eqtrd ( 𝑋 ∈ ( ( V × V ) × V ) → 𝑋 = ⟨ ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) ⟩ , ( 2nd𝑋 ) ⟩ )
10 df-ot ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) , ( 2nd𝑋 ) ⟩ = ⟨ ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) ⟩ , ( 2nd𝑋 ) ⟩
11 9 10 eqtr4di ( 𝑋 ∈ ( ( V × V ) × V ) → 𝑋 = ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) , ( 2nd𝑋 ) ⟩ )
12 3 11 syl ( 𝑋𝑃𝑋 = ⟨ ( 1st ‘ ( 1st𝑋 ) ) , ( 2nd ‘ ( 1st𝑋 ) ) , ( 2nd𝑋 ) ⟩ )