Theorem lsw 14493

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 3488	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6888	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6875	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7405	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6882	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14492	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6979	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 586	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3470  ‘cfv 6529  (class class class)co 7390  1c1 11090   − cmin 11423  ♯chash 14269  lastSclsw 14491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5289  ax-nul 5296  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3430  df-v 3472  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4520  df-sn 4620  df-pr 4622  df-op 4626  df-uni 4899  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6481  df-fun 6531  df-fv 6537  df-ov 7393  df-lsw 14492

This theorem is referenced by:  lsw0  14494  lsw1  14496  lswcl  14497  ccatval1lsw  14513  lswccatn0lsw  14520  swrdlsw  14596  pfxfvlsw  14624  repswlsw  14711  lswcshw  14744  lswco  14769  lsws2  14834  lsws3  14835  lsws4  14836  wrdl2exs2  14876  swrd2lsw  14882  psgnunilem5  19323  wlkonwlk1l  28780  wwlknlsw  28961  wwlksnext  29007  wwlksnredwwlkn  29009  wwlksnextproplem2  29024  clwlkclwwlklem2a1  29105  clwlkclwwlklem2a3  29107  clwlkclwwlklem2a4  29110  clwlkclwwlklem2  29113  clwwisshclwwslem  29127  clwwlknlbonbgr1  29152  clwwlkn2  29157  clwwlkel  29159  clwwlkf  29160  clwwlkwwlksb  29167  clwwlknonex2lem2  29221  2clwwlk2clwwlklem  29459  numclwwlk1lem2f1  29470  pfxlsw2ccat  31982  iwrdsplit  33201  signsvtn0  33396  signstfveq0  33403  lswn0  45870