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

Theorem lsw 12636
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  |-  ( W  e.  X  ->  ( lastS  `  W )  =  ( W `  ( (
# `  W )  -  1 ) ) )

Proof of Theorem lsw
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 elex 3067 . 2  |-  ( W  e.  X  ->  W  e.  _V )
2 fvex 5858 . 2  |-  ( W `
 ( ( # `  W )  -  1 ) )  e.  _V
3 id 22 . . . 4  |-  ( w  =  W  ->  w  =  W )
4 fveq2 5848 . . . . 5  |-  ( w  =  W  ->  ( # `
 w )  =  ( # `  W
) )
54oveq1d 6292 . . . 4  |-  ( w  =  W  ->  (
( # `  w )  -  1 )  =  ( ( # `  W
)  -  1 ) )
63, 5fveq12d 5854 . . 3  |-  ( w  =  W  ->  (
w `  ( ( # `
 w )  - 
1 ) )  =  ( W `  (
( # `  W )  -  1 ) ) )
7 df-lsw 12590 . . 3  |- lastS  =  ( w  e.  _V  |->  ( w `  ( (
# `  w )  -  1 ) ) )
86, 7fvmptg 5929 . 2  |-  ( ( W  e.  _V  /\  ( W `  ( (
# `  W )  -  1 ) )  e.  _V )  -> 
( lastS  `  W )  =  ( W `  (
( # `  W )  -  1 ) ) )
91, 2, 8sylancl 660 1  |-  ( W  e.  X  ->  ( lastS  `  W )  =  ( W `  ( (
# `  W )  -  1 ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    e. wcel 1842   _Vcvv 3058   ` cfv 5568  (class class class)co 6277   1c1 9522    - cmin 9840   #chash 12450   lastS clsw 12582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-iota 5532  df-fun 5570  df-fv 5576  df-ov 6280  df-lsw 12590
This theorem is referenced by:  lsw0  12637  lsw1  12639  lswcl  12640  ccatval1lsw  12654  lswccatn0lsw  12659  swrd0fvlsw  12722  swrdlsw  12731  swrdccatwrd  12747  repswlsw  12808  lswcshw  12837  lswco  12858  swrd2lsw  12944  psgnunilem5  16841  wwlknext  25128  wwlknredwwlkn  25130  wwlkextproplem2  25146  clwwlkgt0  25175  clwwlkn2  25179  clwlkisclwwlklem2a1  25183  clwlkisclwwlklem2a3  25185  clwlkisclwwlklem2a4  25188  clwlkisclwwlklem1  25191  clwwlkel  25197  clwwlkf  25198  clwwisshclwwlem  25210  numclwwlkovf2ex  25490  numclwlk1lem2f1  25498  numclwlk1lem2fo  25499  iwrdsplit  28818  signsvtn0  29019  signstfveq0  29026  lswn0  37847  pfxfvlsw  37871
  Copyright terms: Public domain W3C validator