MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lsw Structured version   Visualization version   GIF version

Definition df-lsw 13255
Description: Extract the last symbol of a word. May be not meaningful for other sets which are not words. The name lastS (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 lastS = (𝑤 ∈ V ↦ (𝑤‘((#‘𝑤) − 1)))

Detailed syntax breakdown of Definition df-lsw
StepHypRef Expression
1 clsw 13247 . 2 class lastS
2 vw . . 3 setvar 𝑤
3 cvv 3190 . . 3 class V
42cv 1479 . . . . . 6 class 𝑤
5 chash 13073 . . . . . 6 class #
64, 5cfv 5857 . . . . 5 class (#‘𝑤)
7 c1 9897 . . . . 5 class 1
8 cmin 10226 . . . . 5 class
96, 7, 8co 6615 . . . 4 class ((#‘𝑤) − 1)
109, 4cfv 5857 . . 3 class (𝑤‘((#‘𝑤) − 1))
112, 3, 10cmpt 4683 . 2 class (𝑤 ∈ V ↦ (𝑤‘((#‘𝑤) − 1)))
121, 11wceq 1480 1 wff lastS = (𝑤 ∈ V ↦ (𝑤‘((#‘𝑤) − 1)))
Colors of variables: wff setvar class
This definition is referenced by:  lsw  13306  sseqval  30273  sseqfv1  30274  sseqfn  30275  sseqf  30277  sseqfv2  30279
  Copyright terms: Public domain W3C validator