Theorem lsw 14599

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 3499	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6920	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6907	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7446	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6914	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14598	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 7014	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 586	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  Vcvv 3478  ‘cfv 6563  (class class class)co 7431  1c1 11154   − cmin 11490  ♯chash 14366  lastSclsw 14597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-iota 6516  df-fun 6565  df-fv 6571  df-ov 7434  df-lsw 14598

This theorem is referenced by:  lsw0  14600  lsw1  14602  lswcl  14603  ccatval1lsw  14619  lswccatn0lsw  14626  swrdlsw  14702  pfxfvlsw  14730  repswlsw  14817  lswcshw  14850  lswco  14875  lsws2  14940  lsws3  14941  lsws4  14942  wrdl2exs2  14982  swrd2lsw  14988  psgnunilem5  19527  wlkonwlk1l  29696  wwlknlsw  29877  wwlksnext  29923  wwlksnredwwlkn  29925  wwlksnextproplem2  29940  clwlkclwwlklem2a1  30021  clwlkclwwlklem2a3  30023  clwlkclwwlklem2a4  30026  clwlkclwwlklem2  30029  clwwisshclwwslem  30043  clwwlknlbonbgr1  30068  clwwlkn2  30073  clwwlkel  30075  clwwlkf  30076  clwwlkwwlksb  30083  clwwlknonex2lem2  30137  2clwwlk2clwwlklem  30375  numclwwlk1lem2f1  30386  pfxlsw2ccat  32920  chnind  32985  chnub  32986  wrdpmtrlast  33096  iwrdsplit  34369  signsvtn0  34564  signstfveq0  34571  lswn0  47369  grtriclwlk3  47850