Definition df-lsw 12543

Description: Extract the last symbol of a word. May be not meaningful for other sets which are not words. The name (as abbreviation of "lastSymbol") is a compromise between usually used names for corresponding functions in computer programs (as last() or lastChar()), the terminology used for words in set.mm ("symbol" instead of "character") and brevity ("lastS" is shorter than "lastChar" and "lastSymbol"). Labels of theorems about last symbols of a word will contain the abbreviation "lsw" (Last Symbol of a Word). (Contributed by Alexander van der Vekens, 18-Mar-2018.)

Assertion

Ref	Expression
df-lsw

Detailed syntax breakdown of Definition df-lsw

Step	Hyp	Ref	Expression
1		clsw 12535	. 2
2		vw	. . 3
3		cvv 3109	. . 3
4	2	cv 1394	. . . . . 6
5		chash 12405	. . . . . 6
6	4, 5	cfv 5593	. . . . 5
7		c1 9514	. . . . 5
8		cmin 9828	. . . . 5
9	6, 7, 8	co 6296	. . . 4
10	9, 4	cfv 5593	. . 3
11	2, 3, 10	cmpt 4510	. 2
12	1, 11	wceq 1395	1

This definition is referenced by:  lsw  12585  sseqval  28327  sseqfv1  28328  sseqfn  28329  sseqf  28331  sseqfv2  28333