Theorem lsw 14621

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 3478	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6898	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 23	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6885	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7434	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6892	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14620	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6991	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 598	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3457  ‘cfv 6540  (class class class)co 7419  1c1 11118   − cmin 11458  ♯chash 14386  lastSclsw 14619

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7422  df-lsw 14620

This theorem is used by:  lsw0  14622  lsw1  14624  lswcl  14625  ccatval1lsw  14642  lswccatn0lsw  14650  swrdlsw  14729  pfxfvlsw  14756  repswlsw  14845  lswcshw  14878  lswco  14902  lsws2  14967  lsws3  14968  lsws4  14969  wrdl2exs2  15009  swrd2lsw  15015  chnind  18701  chnub  18702  chnccats1  18705  chnccat  18706  psgnunilem5  19610  wlkonwlk1l  30071  wwlknlsw  30265  wwlksnext  30311  wwlksnredwwlkn  30313  wwlksnextproplem2  30328  clwlkclwwlklem2a1  30412  clwlkclwwlklem2a3  30414  clwlkclwwlklem2a4  30417  clwlkclwwlklem2  30420  clwwisshclwwslem  30434  clwwlknlbonbgr1  30459  clwwlkn2  30464  clwwlkel  30466  clwwlkf  30467  clwwlkwwlksb  30474  clwwlknonex2lem2  30528  2clwwlk2clwwlklem  30770  numclwwlk1lem2f1  30781  pfxlsw2ccat  33338  wrdpmtrlast  33479  iwrdsplit  34844  signsvtn0  35024  signstfveq0  35031  nthrucw  47667  lswn0  48253  grtriclwlk3  48770