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 P X = 1 st 1 st X 2 nd 1 st X 2 nd X

Proof

Step Hyp Ref Expression
1 mpstssv.p P = mPreSt T
2 1 mpstssv P V × V × V
3 2 sseli X P X V × V × V
4 1st2nd2 X V × V × V X = 1 st X 2 nd X
5 xp1st X V × V × V 1 st X V × V
6 1st2nd2 1 st X V × V 1 st X = 1 st 1 st X 2 nd 1 st X
7 5 6 syl X V × V × V 1 st X = 1 st 1 st X 2 nd 1 st X
8 7 opeq1d X V × V × V 1 st X 2 nd X = 1 st 1 st X 2 nd 1 st X 2 nd X
9 4 8 eqtrd X V × V × V 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 V × V × V X = 1 st 1 st X 2 nd 1 st X 2 nd X
12 3 11 syl X P X = 1 st 1 st X 2 nd 1 st X 2 nd X