Theorem lsw 13915

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 3512	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		fvex 6682	. 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V
3		id 22	. . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊)
4		fveq2 6669	. . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
5	4	oveq1d 7170	. . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
6	3, 5	fveq12d 6676	. . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7		df-lsw 13914	. . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
8	6, 7	fvmptg 6765	. 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
9	1, 2, 8	sylancl 588	1 ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110  Vcvv 3494  ‘cfv 6354  (class class class)co 7155  1c1 10537   − cmin 10869  ♯chash 13689  lastSclsw 13913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-iota 6313  df-fun 6356  df-fv 6362  df-ov 7158  df-lsw 13914

This theorem is referenced by:  lsw0  13916  lsw1  13918  lswcl  13919  ccatval1lsw  13937  lswccatn0lsw  13944  swrdlsw  14028  pfxfvlsw  14056  repswlsw  14143  lswcshw  14176  lswco  14200  lsws2  14265  lsws3  14266  lsws4  14267  wrdl2exs2  14307  swrd2lsw  14313  psgnunilem5  18621  wlkonwlk1l  27444  wwlknlsw  27624  wwlksnext  27670  wwlksnredwwlkn  27672  wwlksnextproplem2  27688  clwlkclwwlklem2a1  27769  clwlkclwwlklem2a3  27771  clwlkclwwlklem2a4  27774  clwlkclwwlklem2  27777  clwwisshclwwslem  27791  clwwlknlbonbgr1  27816  clwwlkn2  27821  clwwlkel  27824  clwwlkf  27825  clwwlkwwlksb  27832  clwwlknonex2lem2  27886  2clwwlk2clwwlklem  28124  numclwwlk1lem2f1  28135  pfxlsw2ccat  30626  iwrdsplit  31645  signsvtn0  31840  signstfveq0  31847  lswn0  43603