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  19438  wlkonwlk1l  29751  wwlknlsw  29936  wwlksnext  29982  wwlksnredwwlkn  29984  wwlksnextproplem2  29999  clwlkclwwlklem2a1  30083  clwlkclwwlklem2a3  30085  clwlkclwwlklem2a4  30088  clwlkclwwlklem2  30091  clwwisshclwwslem  30105  clwwlknlbonbgr1  30130  clwwlkn2  30135  clwwlkel  30137  clwwlkf  30138  clwwlkwwlksb  30145  clwwlknonex2lem2  30199  2clwwlk2clwwlklem  30437  numclwwlk1lem2f1  30448  pfxlsw2ccat  33047  wrdpmtrlast  33191  iwrdsplit  34569  signsvtn0  34752  signstfveq0  34759  nthrucw  47248  lswn0  47808  grtriclwlk3  48309