Theorem lsw 14536

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 3471	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6874	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6861	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7405	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6868	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14535	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6969	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 586	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ‘cfv 6514  (class class class)co 7390  1c1 11076   − cmin 11412  ♯chash 14302  lastSclsw 14534

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-lsw 14535

This theorem is referenced by:  lsw0  14537  lsw1  14539  lswcl  14540  ccatval1lsw  14556  lswccatn0lsw  14563  swrdlsw  14639  pfxfvlsw  14667  repswlsw  14754  lswcshw  14787  lswco  14812  lsws2  14877  lsws3  14878  lsws4  14879  wrdl2exs2  14919  swrd2lsw  14925  psgnunilem5  19431  wlkonwlk1l  29598  wwlknlsw  29784  wwlksnext  29830  wwlksnredwwlkn  29832  wwlksnextproplem2  29847  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a3  29930  clwlkclwwlklem2a4  29933  clwlkclwwlklem2  29936  clwwisshclwwslem  29950  clwwlknlbonbgr1  29975  clwwlkn2  29980  clwwlkel  29982  clwwlkf  29983  clwwlkwwlksb  29990  clwwlknonex2lem2  30044  2clwwlk2clwwlklem  30282  numclwwlk1lem2f1  30293  pfxlsw2ccat  32879  chnind  32944  chnub  32945  chnccats1  32948  wrdpmtrlast  33057  iwrdsplit  34385  signsvtn0  34568  signstfveq0  34575  lswn0  47449  grtriclwlk3  47948