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	$$⊢W\in X\to \mathrm{lastS}\left(W\right)=W\left(\left|W\right|-1\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢W\in X\to W\in \mathrm{V}$$
2		fvex	$$⊢W\left(\left|W\right|-1\right)\in \mathrm{V}$$
3		id	$$⊢w=W\to w=W$$
4		fveq2	$$⊢w=W\to \left|w\right|=\left|W\right|$$
5	4	oveq1d	$$⊢w=W\to \left|w\right|-1=\left|W\right|-1$$
6	3 5	fveq12d	$$⊢w=W\to w\left(\left|w\right|-1\right)=W\left(\left|W\right|-1\right)$$
7		df-lsw	$$⊢\mathrm{lastS}=\left(w\in \mathrm{V}⟼w\left(\left|w\right|-1\right)\right)$$
8	6 7	fvmptg	$$⊢\left(W\in \mathrm{V}\wedge W\left(\left|W\right|-1\right)\in \mathrm{V}\right)\to \mathrm{lastS}\left(W\right)=W\left(\left|W\right|-1\right)$$
9	1 2 8	sylancl	$$⊢W\in X\to \mathrm{lastS}\left(W\right)=W\left(\left|W\right|-1\right)$$