Theorem lsws2

Description: The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021)

	Ref	Expression
Assertion	lsws2	|- ( B e. V -> ( lastS ` <" A B "> ) = B )

Proof

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