Metamath Proof Explorer

Theorem lsws1

Description: The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 s1cl 
 |-  ( A e. V -> <" A "> e. Word V )
2 s1len 
 |-  ( # ` <" A "> ) = 1
3 lsw1 
 |-  ( ( <" A "> e. Word V /\ ( # ` <" A "> ) = 1 ) -> ( lastS ` <" A "> ) = ( <" A "> ` 0 ) )
4 1 2 3 sylancl 
 |-  ( A e. V -> ( lastS ` <" A "> ) = ( <" A "> ` 0 ) )
5 s1fv 
 |-  ( A e. V -> ( <" A "> ` 0 ) = A )
6 4 5 eqtrd 
 |-  ( A e. V -> ( lastS ` <" A "> ) = A )