Theorem lsw 14719

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 3474	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6906	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 23	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6893	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7442	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6900	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14718	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6999	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 598	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  Vcvv 3453  ‘cfv 6546  (class class class)co 7427  1c1 11211   − cmin 11551  ♯chash 14484  lastSclsw 14717

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6500  df-fun 6548  df-fv 6554  df-ov 7430  df-lsw 14718

This theorem is used by:  lsw0  14720  lsw1  14722  lswcl  14723  ccatval1lsw  14740  lswccatn0lsw  14748  swrdlsw  14828  pfxfvlsw  14855  repswlsw  14944  lswcshw  14977  lswco  15001  lsws2  15067  lsws3  15068  lsws4  15069  wrdl2exs2  15109  swrd2lsw  15117  chnind  18807  chnub  18808  chnccats1  18811  chnccat  18812  psgnunilem5  19720  wlkonwlk1l  30254  wwlknlsw  30448  wwlksnext  30494  wwlksnredwwlkn  30496  wwlksnextproplem2  30511  clwlkclwwlklem2a1  30595  clwlkclwwlklem2a3  30597  clwlkclwwlklem2a4  30600  clwlkclwwlklem2  30603  clwwisshclwwslem  30617  clwwlknlbonbgr1  30642  clwwlkn2  30647  clwwlkel  30649  clwwlkf  30650  clwwlkwwlksb  30657  clwwlknonex2lem2  30711  2clwwlk2clwwlklem  30959  numclwwlk1lem2f1  30970  pfxlsw2ccat  33566  wrdpmtrlast  33707  iwrdsplit  35072  signsvtn0  35252  signstfveq0  35259  numtowerdt  48055  lswn0  48665  grtriclwlk3  49182