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 
|- P = ( mPreSt ` T )
Assertion mpst123 
|- ( X e. P -> X = <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) , ( 2nd ` X ) >. )

Proof

Step Hyp Ref Expression
1 mpstssv.p 
 |-  P = ( mPreSt ` T )
2 1 mpstssv 
 |-  P C_ ( ( _V X. _V ) X. _V )
3 2 sseli 
 |-  ( X e. P -> X e. ( ( _V X. _V ) X. _V ) )
4 1st2nd2 
 |-  ( X e. ( ( _V X. _V ) X. _V ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
5 xp1st 
 |-  ( X e. ( ( _V X. _V ) X. _V ) -> ( 1st ` X ) e. ( _V X. _V ) )
6 1st2nd2 
 |-  ( ( 1st ` X ) e. ( _V X. _V ) -> ( 1st ` X ) = <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) >. )
7 5 6 syl 
 |-  ( X e. ( ( _V X. _V ) X. _V ) -> ( 1st ` X ) = <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) >. )
8 7 opeq1d 
 |-  ( X e. ( ( _V X. _V ) X. _V ) -> <. ( 1st ` X ) , ( 2nd ` X ) >. = <. <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) >. , ( 2nd ` X ) >. )
9 4 8 eqtrd 
 |-  ( X e. ( ( _V X. _V ) X. _V ) -> X = <. <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) >. , ( 2nd ` X ) >. )
10 df-ot 
 |-  <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) , ( 2nd ` X ) >. = <. <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) >. , ( 2nd ` X ) >.
11 9 10 eqtr4di 
 |-  ( X e. ( ( _V X. _V ) X. _V ) -> X = <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) , ( 2nd ` X ) >. )
12 3 11 syl 
 |-  ( X e. P -> X = <. ( 1st ` ( 1st ` X ) ) , ( 2nd ` ( 1st ` X ) ) , ( 2nd ` X ) >. )