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

Theorem lsw 13059
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 3089 . 2 (𝑊𝑋𝑊 ∈ V)
2 fvex 5996 . 2 (𝑊‘((#‘𝑊) − 1)) ∈ V
3 id 22 . . . 4 (𝑤 = 𝑊𝑤 = 𝑊)
4 fveq2 5986 . . . . 5 (𝑤 = 𝑊 → (#‘𝑤) = (#‘𝑊))
54oveq1d 6440 . . . 4 (𝑤 = 𝑊 → ((#‘𝑤) − 1) = ((#‘𝑊) − 1))
63, 5fveq12d 5992 . . 3 (𝑤 = 𝑊 → (𝑤‘((#‘𝑤) − 1)) = (𝑊‘((#‘𝑊) − 1)))
7 df-lsw 13010 . . 3 lastS = (𝑤 ∈ V ↦ (𝑤‘((#‘𝑤) − 1)))
86, 7fvmptg 6072 . 2 ((𝑊 ∈ V ∧ (𝑊‘((#‘𝑊) − 1)) ∈ V) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1)))
91, 2, 8sylancl 692 1 (𝑊𝑋 → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1938  Vcvv 3077  cfv 5689  (class class class)co 6425  1c1 9690  cmin 10015  #chash 12844   lastS clsw 13002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-iota 5653  df-fun 5691  df-fv 5697  df-ov 6428  df-lsw 13010
This theorem is referenced by:  lsw0  13060  lsw1  13062  lswcl  13063  ccatval1lsw  13076  lswccatn0lsw  13081  swrd0fvlsw  13150  swrdlsw  13159  swrdccatwrd  13175  repswlsw  13235  lswcshw  13267  lswco  13290  lsws2  13354  lsws3  13355  lsws4  13356  wrdl2exs2  13393  swrd2lsw  13398  psgnunilem5  17650  wwlknext  26020  wwlknredwwlkn  26022  wwlkextproplem2  26038  clwwlkgt0  26067  clwwlkn2  26071  clwlkisclwwlklem2a1  26075  clwlkisclwwlklem2a3  26077  clwlkisclwwlklem2a4  26080  clwlkisclwwlklem1  26083  clwwlkel  26089  clwwlkf  26090  clwwisshclwwlem  26102  numclwwlkovf2ex  26381  numclwlk1lem2f1  26389  numclwlk1lem2fo  26390  iwrdsplit  29613  signsvtn0  29848  signstfveq0  29855  lswn0  40152  pfxfvlsw  40176  wlkOnwlk1l  40978  wwlksnext  41206  wwlksnredwwlkn  41208  wwlksnextproplem2  41223  clwlkclwwlklem2a1  41308  clwlkclwwlklem2a3  41310  clwlkclwwlklem2a4  41313  clwlkclwwlklem2  41316  clwwlksn2  41324  clwwlksel  41328  clwwlksf  41329  clwwisshclwwslem  41341  av-numclwwlkovf2ex  41624  av-numclwlk1lem2f1  41631  av-numclwlk1lem2fo  41632
  Copyright terms: Public domain W3C validator