Theorem lsw 13964

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 3429	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6672	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6659	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7166	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6666	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 13963	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6758	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 590	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  Vcvv 3410  ‘cfv 6336  (class class class)co 7151  1c1 10577   − cmin 10909  ♯chash 13741  lastSclsw 13962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-iota 6295  df-fun 6338  df-fv 6344  df-ov 7154  df-lsw 13963

This theorem is referenced by:  lsw0  13965  lsw1  13967  lswcl  13968  ccatval1lsw  13986  lswccatn0lsw  13993  swrdlsw  14077  pfxfvlsw  14105  repswlsw  14192  lswcshw  14225  lswco  14249  lsws2  14314  lsws3  14315  lsws4  14316  wrdl2exs2  14356  swrd2lsw  14362  psgnunilem5  18690  wlkonwlk1l  27553  wwlknlsw  27733  wwlksnext  27779  wwlksnredwwlkn  27781  wwlksnextproplem2  27796  clwlkclwwlklem2a1  27877  clwlkclwwlklem2a3  27879  clwlkclwwlklem2a4  27882  clwlkclwwlklem2  27885  clwwisshclwwslem  27899  clwwlknlbonbgr1  27924  clwwlkn2  27929  clwwlkel  27931  clwwlkf  27932  clwwlkwwlksb  27939  clwwlknonex2lem2  27993  2clwwlk2clwwlklem  28231  numclwwlk1lem2f1  28242  pfxlsw2ccat  30749  iwrdsplit  31874  signsvtn0  32069  signstfveq0  32076  lswn0  44330