Theorem lsw 14632

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 3471	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6892	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 23	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6879	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7429	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6886	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14631	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6985	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 598	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3450  ‘cfv 6533  (class class class)co 7414  1c1 11128   − cmin 11468  ♯chash 14397  lastSclsw 14630

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7417  df-lsw 14631

This theorem is used by:  lsw0  14633  lsw1  14635  lswcl  14636  ccatval1lsw  14653  lswccatn0lsw  14661  swrdlsw  14740  pfxfvlsw  14767  repswlsw  14856  lswcshw  14889  lswco  14913  lsws2  14978  lsws3  14979  lsws4  14980  wrdl2exs2  15020  swrd2lsw  15028  chnind  18712  chnub  18713  chnccats1  18716  chnccat  18717  psgnunilem5  19624  wlkonwlk1l  30124  wwlknlsw  30318  wwlksnext  30364  wwlksnredwwlkn  30366  wwlksnextproplem2  30381  clwlkclwwlklem2a1  30465  clwlkclwwlklem2a3  30467  clwlkclwwlklem2a4  30470  clwlkclwwlklem2  30473  clwwisshclwwslem  30487  clwwlknlbonbgr1  30512  clwwlkn2  30517  clwwlkel  30519  clwwlkf  30520  clwwlkwwlksb  30527  clwwlknonex2lem2  30581  2clwwlk2clwwlklem  30829  numclwwlk1lem2f1  30840  pfxlsw2ccat  33395  wrdpmtrlast  33536  iwrdsplit  34901  signsvtn0  35081  signstfveq0  35088  numtowerdt  47737  lswn0  48347  grtriclwlk3  48864