Theorem lsw 14499

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 3463	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6855	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6842	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7383	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6849	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14498	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6947	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 587	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ‘cfv 6500  (class class class)co 7368  1c1 11039   − cmin 11376  ♯chash 14265  lastSclsw 14497

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-lsw 14498

This theorem is referenced by:  lsw0  14500  lsw1  14502  lswcl  14503  ccatval1lsw  14520  lswccatn0lsw  14527  swrdlsw  14603  pfxfvlsw  14630  repswlsw  14717  lswcshw  14750  lswco  14774  lsws2  14839  lsws3  14840  lsws4  14841  wrdl2exs2  14881  swrd2lsw  14887  chnind  18556  chnub  18557  chnccats1  18560  chnccat  18561  psgnunilem5  19435  wlkonwlk1l  29747  wwlknlsw  29932  wwlksnext  29978  wwlksnredwwlkn  29980  wwlksnextproplem2  29995  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a3  30081  clwlkclwwlklem2a4  30084  clwlkclwwlklem2  30087  clwwisshclwwslem  30101  clwwlknlbonbgr1  30126  clwwlkn2  30131  clwwlkel  30133  clwwlkf  30134  clwwlkwwlksb  30141  clwwlknonex2lem2  30195  2clwwlk2clwwlklem  30433  numclwwlk1lem2f1  30444  pfxlsw2ccat  33043  wrdpmtrlast  33187  iwrdsplit  34565  signsvtn0  34748  signstfveq0  34755  nthrucw  47244  lswn0  47804  grtriclwlk3  48305