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 ‘ 𝑋 ) 〉 ) |