![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lsw | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
lsw | ⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3464 | . 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) | |
2 | fvex 6860 | . 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V | |
3 | id 22 | . . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) | |
4 | fveq2 6847 | . . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊)) | |
5 | 4 | oveq1d 7377 | . . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1)) |
6 | 3, 5 | fveq12d 6854 | . . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1))) |
7 | df-lsw 14463 | . . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1))) | |
8 | 6, 7 | fvmptg 6951 | . 2 ⊢ ((𝑊 ∈ V ∧ (𝑊‘((♯‘𝑊) − 1)) ∈ V) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
9 | 1, 2, 8 | sylancl 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 |