MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lsw Structured version   Visualization version   GIF version

Theorem lsw 14464
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.
StepHypRef Expression
1 elex 3464 . 2 (𝑊𝑋𝑊 ∈ V)
2 fvex 6860 . 2 (𝑊‘((♯‘𝑊) − 1)) ∈ V
3 id 22 . . . 4 (𝑤 = 𝑊𝑤 = 𝑊)
4 fveq2 6847 . . . . 5 (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
54oveq1d 7377 . . . 4 (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
63, 5fveq12d 6854 . . 3 (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7 df-lsw 14463 . . 3 lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
86, 7fvmptg 6951 . 2 ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
91, 2, 8sylancl 586 1 (𝑊𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  Vcvv 3446  cfv 6501  (class class class)co 7362  1c1 11061  cmin 11394  chash 14240  lastSclsw 14462
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-ov 7365  df-lsw 14463
This theorem is referenced by:  lsw0  14465  lsw1  14467  lswcl  14468  ccatval1lsw  14484  lswccatn0lsw  14491  swrdlsw  14567  pfxfvlsw  14595  repswlsw  14682  lswcshw  14715  lswco  14740  lsws2  14805  lsws3  14806  lsws4  14807  wrdl2exs2  14847  swrd2lsw  14853  psgnunilem5  19290  wlkonwlk1l  28674  wwlknlsw  28855  wwlksnext  28901  wwlksnredwwlkn  28903  wwlksnextproplem2  28918  clwlkclwwlklem2a1  28999  clwlkclwwlklem2a3  29001  clwlkclwwlklem2a4  29004  clwlkclwwlklem2  29007  clwwisshclwwslem  29021  clwwlknlbonbgr1  29046  clwwlkn2  29051  clwwlkel  29053  clwwlkf  29054  clwwlkwwlksb  29061  clwwlknonex2lem2  29115  2clwwlk2clwwlklem  29353  numclwwlk1lem2f1  29364  pfxlsw2ccat  31876  iwrdsplit  33076  signsvtn0  33271  signstfveq0  33278  lswn0  45756
  Copyright terms: Public domain W3C validator