| 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 3501 | . 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) | |
| 2 | fvex 6919 | . 2 ⊢ (𝑊‘((♯‘𝑊) − 1)) ∈ V | |
| 3 | id 22 | . . . 4 ⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) | |
| 4 | fveq2 6906 | . . . . 5 ⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊)) | |
| 5 | 4 | oveq1d 7446 | . . . 4 ⊢ (𝑤 = 𝑊 → ((♯‘𝑤) − 1) = ((♯‘𝑊) − 1)) |
| 6 | 3, 5 | fveq12d 6913 | . . 3 ⊢ (𝑤 = 𝑊 → (𝑤‘((♯‘𝑤) − 1)) = (𝑊‘((♯‘𝑊) − 1))) |
| 7 | df-lsw 14601 | . . 3 ⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1))) | |
| 8 | 6, 7 | fvmptg 7014 | . 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 1540 ∈ wcel 2108 Vcvv 3480 ‘cfv 6561 (class class class)co 7431 1c1 11156 − cmin 11492 ♯chash 14369 lastSclsw 14600 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-iota 6514 df-fun 6563 df-fv 6569 df-ov 7434 df-lsw 14601 |
| This theorem is referenced by: lsw0 14603 lsw1 14605 lswcl 14606 ccatval1lsw 14622 lswccatn0lsw 14629 swrdlsw 14705 pfxfvlsw 14733 repswlsw 14820 lswcshw 14853 lswco 14878 lsws2 14943 lsws3 14944 lsws4 14945 wrdl2exs2 14985 swrd2lsw 14991 psgnunilem5 19512 wlkonwlk1l 29681 wwlknlsw 29867 wwlksnext 29913 wwlksnredwwlkn 29915 wwlksnextproplem2 29930 clwlkclwwlklem2a1 30011 clwlkclwwlklem2a3 30013 clwlkclwwlklem2a4 30016 clwlkclwwlklem2 30019 clwwisshclwwslem 30033 clwwlknlbonbgr1 30058 clwwlkn2 30063 clwwlkel 30065 clwwlkf 30066 clwwlkwwlksb 30073 clwwlknonex2lem2 30127 2clwwlk2clwwlklem 30365 numclwwlk1lem2f1 30376 pfxlsw2ccat 32935 chnind 33001 chnub 33002 chnccats1 33005 wrdpmtrlast 33113 iwrdsplit 34389 signsvtn0 34585 signstfveq0 34592 lswn0 47431 grtriclwlk3 47912 |
| Copyright terms: Public domain | W3C validator |