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

Theorem lsw 13908
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 3511 . 2 (𝑊𝑋𝑊 ∈ V)
2 fvex 6676 . 2 (𝑊‘((♯‘𝑊) − 1)) ∈ V
3 id 22 . . . 4 (𝑤 = 𝑊𝑤 = 𝑊)
4 fveq2 6663 . . . . 5 (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊))
54oveq1d 7163 . . . 4 (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1))
63, 5fveq12d 6670 . . 3 (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
7 df-lsw 13907 . . 3 lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
86, 7fvmptg 6759 . 2 ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
91, 2, 8sylancl 588 1 (𝑊𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1531  wcel 2108  Vcvv 3493  cfv 6348  (class class class)co 7148  1c1 10530  cmin 10862  chash 13682  lastSclsw 13906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7151  df-lsw 13907
This theorem is referenced by:  lsw0  13909  lsw1  13911  lswcl  13912  ccatval1lsw  13930  lswccatn0lsw  13937  swrdlsw  14021  pfxfvlsw  14049  repswlsw  14136  lswcshw  14169  lswco  14193  lsws2  14258  lsws3  14259  lsws4  14260  wrdl2exs2  14300  swrd2lsw  14306  psgnunilem5  18614  wlkonwlk1l  27437  wwlknlsw  27617  wwlksnext  27663  wwlksnredwwlkn  27665  wwlksnextproplem2  27681  clwlkclwwlklem2a1  27762  clwlkclwwlklem2a3  27764  clwlkclwwlklem2a4  27767  clwlkclwwlklem2  27770  clwwisshclwwslem  27784  clwwlknlbonbgr1  27809  clwwlkn2  27814  clwwlkel  27817  clwwlkf  27818  clwwlkwwlksb  27825  clwwlknonex2lem2  27879  2clwwlk2clwwlklem  28117  numclwwlk1lem2f1  28128  pfxlsw2ccat  30619  iwrdsplit  31638  signsvtn0  31833  signstfveq0  31840  lswn0  43594
  Copyright terms: Public domain W3C validator