Theorem lsw 14485

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 3459	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6845	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6832	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7371	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6839	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14484	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6937	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 586	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3438  ‘cfv 6490  (class class class)co 7356  1c1 11025   − cmin 11362  ♯chash 14251  lastSclsw 14483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-iota 6446  df-fun 6492  df-fv 6498  df-ov 7359  df-lsw 14484

This theorem is referenced by:  lsw0  14486  lsw1  14488  lswcl  14489  ccatval1lsw  14506  lswccatn0lsw  14513  swrdlsw  14589  pfxfvlsw  14616  repswlsw  14703  lswcshw  14736  lswco  14760  lsws2  14825  lsws3  14826  lsws4  14827  wrdl2exs2  14867  swrd2lsw  14873  chnind  18542  chnub  18543  chnccats1  18546  chnccat  18547  psgnunilem5  19421  wlkonwlk1l  29684  wwlknlsw  29869  wwlksnext  29915  wwlksnredwwlkn  29917  wwlksnextproplem2  29932  clwlkclwwlklem2a1  30016  clwlkclwwlklem2a3  30018  clwlkclwwlklem2a4  30021  clwlkclwwlklem2  30024  clwwisshclwwslem  30038  clwwlknlbonbgr1  30063  clwwlkn2  30068  clwwlkel  30070  clwwlkf  30071  clwwlkwwlksb  30078  clwwlknonex2lem2  30132  2clwwlk2clwwlklem  30370  numclwwlk1lem2f1  30381  pfxlsw2ccat  32981  wrdpmtrlast  33124  iwrdsplit  34493  signsvtn0  34676  signstfveq0  34683  nthrucw  47072  lswn0  47632  grtriclwlk3  48133