Theorem lsw 14487

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 3461	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6847	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6834	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7373	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6841	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14486	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6939	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 586	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ‘cfv 6492  (class class class)co 7358  1c1 11027   − cmin 11364  ♯chash 14253  lastSclsw 14485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-lsw 14486

This theorem is referenced by:  lsw0  14488  lsw1  14490  lswcl  14491  ccatval1lsw  14508  lswccatn0lsw  14515  swrdlsw  14591  pfxfvlsw  14618  repswlsw  14705  lswcshw  14738  lswco  14762  lsws2  14827  lsws3  14828  lsws4  14829  wrdl2exs2  14869  swrd2lsw  14875  chnind  18544  chnub  18545  chnccats1  18548  chnccat  18549  psgnunilem5  19423  wlkonwlk1l  29735  wwlknlsw  29920  wwlksnext  29966  wwlksnredwwlkn  29968  wwlksnextproplem2  29983  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a3  30069  clwlkclwwlklem2a4  30072  clwlkclwwlklem2  30075  clwwisshclwwslem  30089  clwwlknlbonbgr1  30114  clwwlkn2  30119  clwwlkel  30121  clwwlkf  30122  clwwlkwwlksb  30129  clwwlknonex2lem2  30183  2clwwlk2clwwlklem  30421  numclwwlk1lem2f1  30432  pfxlsw2ccat  33032  wrdpmtrlast  33175  iwrdsplit  34544  signsvtn0  34727  signstfveq0  34734  nthrucw  47140  lswn0  47700  grtriclwlk3  48201