Theorem lsw 14520

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 3451	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6848	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6835	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7376	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6842	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14519	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6940	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 587	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ‘cfv 6493  (class class class)co 7361  1c1 11033   − cmin 11371  ♯chash 14286  lastSclsw 14518

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 5232  ax-nul 5242  ax-pr 5371

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-ov 7364  df-lsw 14519

This theorem is referenced by:  lsw0  14521  lsw1  14523  lswcl  14524  ccatval1lsw  14541  lswccatn0lsw  14548  swrdlsw  14624  pfxfvlsw  14651  repswlsw  14738  lswcshw  14771  lswco  14795  lsws2  14860  lsws3  14861  lsws4  14862  wrdl2exs2  14902  swrd2lsw  14908  chnind  18581  chnub  18582  chnccats1  18585  chnccat  18586  psgnunilem5  19463  wlkonwlk1l  29748  wwlknlsw  29933  wwlksnext  29979  wwlksnredwwlkn  29981  wwlksnextproplem2  29996  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a3  30082  clwlkclwwlklem2a4  30085  clwlkclwwlklem2  30088  clwwisshclwwslem  30102  clwwlknlbonbgr1  30127  clwwlkn2  30132  clwwlkel  30134  clwwlkf  30135  clwwlkwwlksb  30142  clwwlknonex2lem2  30196  2clwwlk2clwwlklem  30434  numclwwlk1lem2f1  30445  pfxlsw2ccat  33028  wrdpmtrlast  33172  iwrdsplit  34550  signsvtn0  34733  signstfveq0  34740  nthrucw  47335  lswn0  47919  grtriclwlk3  48436