Theorem lsw 14602

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 3501	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6919	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6906	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7446	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6913	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14601	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 7014	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 586	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ‘cfv 6561  (class class class)co 7431  1c1 11156   − cmin 11492  ♯chash 14369  lastSclsw 14600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-lsw 14601

This theorem is referenced by:  lsw0  14603  lsw1  14605  lswcl  14606  ccatval1lsw  14622  lswccatn0lsw  14629  swrdlsw  14705  pfxfvlsw  14733  repswlsw  14820  lswcshw  14853  lswco  14878  lsws2  14943  lsws3  14944  lsws4  14945  wrdl2exs2  14985  swrd2lsw  14991  psgnunilem5  19512  wlkonwlk1l  29681  wwlknlsw  29867  wwlksnext  29913  wwlksnredwwlkn  29915  wwlksnextproplem2  29930  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a3  30013  clwlkclwwlklem2a4  30016  clwlkclwwlklem2  30019  clwwisshclwwslem  30033  clwwlknlbonbgr1  30058  clwwlkn2  30063  clwwlkel  30065  clwwlkf  30066  clwwlkwwlksb  30073  clwwlknonex2lem2  30127  2clwwlk2clwwlklem  30365  numclwwlk1lem2f1  30376  pfxlsw2ccat  32935  chnind  33001  chnub  33002  chnccats1  33005  wrdpmtrlast  33113  iwrdsplit  34389  signsvtn0  34585  signstfveq0  34592  lswn0  47431  grtriclwlk3  47912