Step |
Hyp |
Ref |
Expression |
1 |
|
s3cli |
|- <" A B C "> e. Word _V |
2 |
|
lsw |
|- ( <" A B C "> e. Word _V -> ( lastS ` <" A B C "> ) = ( <" A B C "> ` ( ( # ` <" A B C "> ) - 1 ) ) ) |
3 |
1 2
|
mp1i |
|- ( C e. V -> ( lastS ` <" A B C "> ) = ( <" A B C "> ` ( ( # ` <" A B C "> ) - 1 ) ) ) |
4 |
|
s3len |
|- ( # ` <" A B C "> ) = 3 |
5 |
4
|
oveq1i |
|- ( ( # ` <" A B C "> ) - 1 ) = ( 3 - 1 ) |
6 |
|
3m1e2 |
|- ( 3 - 1 ) = 2 |
7 |
5 6
|
eqtri |
|- ( ( # ` <" A B C "> ) - 1 ) = 2 |
8 |
7
|
fveq2i |
|- ( <" A B C "> ` ( ( # ` <" A B C "> ) - 1 ) ) = ( <" A B C "> ` 2 ) |
9 |
8
|
a1i |
|- ( C e. V -> ( <" A B C "> ` ( ( # ` <" A B C "> ) - 1 ) ) = ( <" A B C "> ` 2 ) ) |
10 |
|
s3fv2 |
|- ( C e. V -> ( <" A B C "> ` 2 ) = C ) |
11 |
3 9 10
|
3eqtrd |
|- ( C e. V -> ( lastS ` <" A B C "> ) = C ) |