Metamath Proof Explorer


Theorem lsw

Description: Extract the last symbol of a word. May be not meaningful for other sets which are not words. (Contributed by Alexander van der Vekens, 18-Mar-2018)

Ref Expression
Assertion lsw WXlastSW=WW1

Proof

Step Hyp Ref Expression
1 elex WXWV
2 fvex WW1V
3 id w=Ww=W
4 fveq2 w=Ww=W
5 4 oveq1d w=Ww1=W1
6 3 5 fveq12d w=Www1=WW1
7 df-lsw lastS=wVww1
8 6 7 fvmptg WVWW1VlastSW=WW1
9 1 2 8 sylancl WXlastSW=WW1