Theorem lsw 14587

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.)

Assertion

Ref	Expression
lsw	⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Proof of Theorem lsw

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3485	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6894	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6881	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7425	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6888	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14586	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6989	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 586	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3464  ‘cfv 6536  (class class class)co 7410  1c1 11135   − cmin 11471  ♯chash 14353  lastSclsw 14585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6538  df-fv 6544  df-ov 7413  df-lsw 14586

This theorem is referenced by:  lsw0  14588  lsw1  14590  lswcl  14591  ccatval1lsw  14607  lswccatn0lsw  14614  swrdlsw  14690  pfxfvlsw  14718  repswlsw  14805  lswcshw  14838  lswco  14863  lsws2  14928  lsws3  14929  lsws4  14930  wrdl2exs2  14970  swrd2lsw  14976  psgnunilem5  19480  wlkonwlk1l  29648  wwlknlsw  29834  wwlksnext  29880  wwlksnredwwlkn  29882  wwlksnextproplem2  29897  clwlkclwwlklem2a1  29978  clwlkclwwlklem2a3  29980  clwlkclwwlklem2a4  29983  clwlkclwwlklem2  29986  clwwisshclwwslem  30000  clwwlknlbonbgr1  30025  clwwlkn2  30030  clwwlkel  30032  clwwlkf  30033  clwwlkwwlksb  30040  clwwlknonex2lem2  30094  2clwwlk2clwwlklem  30332  numclwwlk1lem2f1  30343  pfxlsw2ccat  32931  chnind  32996  chnub  32997  chnccats1  33000  wrdpmtrlast  33109  iwrdsplit  34424  signsvtn0  34607  signstfveq0  34614  lswn0  47425  grtriclwlk3  47924