Theorem lsw 14709

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 3472	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6898	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 23	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6885	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7435	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6892	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 14708	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6991	. 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 3451  ‘cfv 6538  (class class class)co 7420  1c1 11201   − cmin 11541  ♯chash 14474  lastSclsw 14707

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-lsw 14708

This theorem is used by:  lsw0  14710  lsw1  14712  lswcl  14713  ccatval1lsw  14730  lswccatn0lsw  14738  swrdlsw  14817  pfxfvlsw  14844  repswlsw  14933  lswcshw  14966  lswco  14990  lsws2  15055  lsws3  15056  lsws4  15057  wrdl2exs2  15097  swrd2lsw  15105  chnind  18795  chnub  18796  chnccats1  18799  chnccat  18800  psgnunilem5  19708  wlkonwlk1l  30242  wwlknlsw  30436  wwlksnext  30482  wwlksnredwwlkn  30484  wwlksnextproplem2  30499  clwlkclwwlklem2a1  30583  clwlkclwwlklem2a3  30585  clwlkclwwlklem2a4  30588  clwlkclwwlklem2  30591  clwwisshclwwslem  30605  clwwlknlbonbgr1  30630  clwwlkn2  30635  clwwlkel  30637  clwwlkf  30638  clwwlkwwlksb  30645  clwwlknonex2lem2  30699  2clwwlk2clwwlklem  30947  numclwwlk1lem2f1  30958  pfxlsw2ccat  33513  wrdpmtrlast  33654  iwrdsplit  35019  signsvtn0  35199  signstfveq0  35206  numtowerdt  47915  lswn0  48525  grtriclwlk3  49042