Theorem lsw 14464

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 3464	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6860	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6847	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7377	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6854	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14463	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6951	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 586	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3446  ‘cfv 6501  (class class class)co 7362  1c1 11061   − cmin 11394  ♯chash 14240  lastSclsw 14462

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 5261  ax-nul 5268  ax-pr 5389

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 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-ov 7365  df-lsw 14463

This theorem is referenced by:  lsw0  14465  lsw1  14467  lswcl  14468  ccatval1lsw  14484  lswccatn0lsw  14491  swrdlsw  14567  pfxfvlsw  14595  repswlsw  14682  lswcshw  14715  lswco  14740  lsws2  14805  lsws3  14806  lsws4  14807  wrdl2exs2  14847  swrd2lsw  14853  psgnunilem5  19290  wlkonwlk1l  28674  wwlknlsw  28855  wwlksnext  28901  wwlksnredwwlkn  28903  wwlksnextproplem2  28918  clwlkclwwlklem2a1  28999  clwlkclwwlklem2a3  29001  clwlkclwwlklem2a4  29004  clwlkclwwlklem2  29007  clwwisshclwwslem  29021  clwwlknlbonbgr1  29046  clwwlkn2  29051  clwwlkel  29053  clwwlkf  29054  clwwlkwwlksb  29061  clwwlknonex2lem2  29115  2clwwlk2clwwlklem  29353  numclwwlk1lem2f1  29364  pfxlsw2ccat  31876  iwrdsplit  33076  signsvtn0  33271  signstfveq0  33278  lswn0  45756