lencl - Metamath Proof Explorer

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

Theorem lencl 14483

Description: The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015.)

**Assertion**
Ref	Expression
lencl	⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ₀)

**Proof of Theorem lencl**
Step	Hyp	Ref	Expression
1		wrdfin 14482	. 2 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin)
2		hashcl 14316	. 2 ⊢ (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ₀)
3	1, 2	syl 17	1 ⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ₀)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2107 ‘cfv 6544 Fincfn 8939 ℕ₀cn0 12472 ♯chash 14290 Word cword 14464

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-n0 12473 df-z 12559 df-uz 12823 df-fz 13485 df-fzo 13628 df-hash 14291 df-word 14465

This theorem is referenced by: wrdffz 14485 wrdnfi 14498 wrdsymb0 14499 wrdlenge1n0 14500 wrdlenge2n0 14502 wrdsymb1 14503 eqwrd 14507 wrdred1 14510 wrdred1hash 14511 ccatcl 14524 ccatlen 14525 ccat0 14526 ccatval1 14527 ccatval3 14529 elfzelfzccat 14530 ccatsymb 14532 ccatfv0 14533 ccatval21sw 14535 ccatlid 14536 ccatrid 14537 ccatass 14538 ccatrn 14539 lswccatn0lsw 14541 ccatalpha 14543 ccatws1lenp1b 14571 wrdlenccats1lenm1 14572 ccatw2s1len 14575 ccats1val2 14577 ccatws1n0 14582 lswccats1fst 14585 ccatw2s1p1 14586 ccat2s1fvw 14588 swrdnd 14604 swrdnd2 14605 swrdnd0 14607 swrdrlen 14609 swrdlen2 14610 swrdfv2 14611 swrdlsw 14617 swrdccat2 14619 pfxid 14634 pfxn0 14636 pfxnd0 14638 addlenrevpfx 14640 addlenpfx 14641 pfxtrcfv0 14644 pfxeq 14646 pfxtrcfvl 14647 pfxsuffeqwrdeq 14648 pfxccat1 14652 pfxcctswrd 14660 ccats1pfxeq 14664 ccats1pfxeqrex 14665 ccatopth2 14667 cats1un 14671 wrdind 14672 wrd2ind 14673 swrdccatin1 14675 swrdccatin2 14679 pfxccatin12lem2 14681 pfxccatin12lem3 14682 pfxccatin12 14683 pfxccat3 14684 swrdccat 14685 pfxccatpfx2 14687 pfxccat3a 14688 swrdccat3blem 14689 swrdccat3b 14690 pfxccatid 14691 ccats1pfxeqbi 14692 spllen 14704 splfv1 14705 splfv2a 14706 splval2 14707 revcl 14711 revlen 14712 revccat 14716 revrev 14717 repswsymball 14729 repswsymballbi 14730 cshw0 14744 cshwsublen 14746 cshwn 14747 cshwlen 14749 cshwidxmod 14753 2cshwid 14764 3cshw 14768 cshweqdif2 14769 cshw1 14772 scshwfzeqfzo 14777 revco 14785 ccatco 14786 cats1fvn 14809 cats1fv 14810 pfx2 14898 swrd2lsw 14903 2swrd2eqwrdeq 14904 ccat2s1fvwALT 14906 cshwshashnsame 17037 gsmsymgrfixlem1 19295 gsmsymgreqlem2 19299 pmtrdifwrdellem2 19350 psgnuni 19367 psgnran 19383 efginvrel2 19595 efgsdmi 19600 efgsval2 19601 efgsp1 19605 efgsfo 19607 efgredlemf 19609 efgredlemg 19610 efgredleme 19611 efgredlemd 19612 efgredlemc 19613 efgredlem 19615 efgred 19616 efgcpbllemb 19623 frgpuplem 19640 frgpnabllem1 19741 pgpfaclem1 19951 psgnghm 21133 upgrewlkle2 28863 wlkcl 28872 wlkeq 28891 wlkv0 28908 wlklenvclwlk 28912 redwlklem 28928 wlkp1lem3 28932 wlkp1lem8 28937 wlkdlem1 28939 pthdlem1 29023 pthdlem2 29025 wlkiswwlks1 29121 wlkiswwlks2lem1 29123 wlkiswwlks2lem3 29125 wlkiswwlks2lem4 29126 wwlksm1edg 29135 wlklnwwlkln2lem 29136 wwlksnextbi 29148 wwlksnextproplem2 29164 wwlksnextproplem3 29165 rusgrnumwwlks 29228 clwwlkccatlem 29242 umgrclwwlkge2 29244 clwlkclwwlklem2a1 29245 clwlkclwwlklem2a2 29246 clwlkclwwlklem2a4 29250 clwlkclwwlklem2a 29251 clwlkclwwlklem2 29253 clwlkclwwlklem3 29254 clwlkclwwlk 29255 clwlkclwwlk2 29256 clwlkclwwlkfo 29262 clwwisshclwwslem 29267 erclwwlkref 29273 clwwlkn 29279 clwwlkwwlksb 29307 clwlknf1oclwwlknlem1 29334 clwwlknonex2lem2 29361 eupth2eucrct 29470 eucrctshift 29496 numclwlk2lem2f1o 29632 ccatf1 32115 pfxlsw2ccat 32116 wrdt2ind 32117 splfv3 32122 cycpmfv1 32272 cycpmfv2 32273 cycpmco2f1 32283 cycpmco2rn 32284 cycpmco2lem3 32287 cycpmco2lem4 32288 cycpmco2lem5 32289 cycpmco2lem6 32290 cycpmco2lem7 32291 cycpmco2 32292 cycpmrn 32302 cyc3genpm 32311 sseqfv1 33388 sseqfn 33389 sseqmw 33390 sseqf 33391 sseqfv2 33393 sseqp1 33394 ofcccat 33554 signstlen 33578 signstfvn 33580 signstfvp 33582 signstfvneq0 33583 signstfvc 33585 signstfveq0a 33587 signstfveq0 33588 signshf 33599 signshlen 33601 signshnz 33602 lpadlem3 33690 lpadlem2 33692 lpadlen2 33693 lpadmax 33694 lpadleft 33695 lpadright 33696 revpfxsfxrev 34106 revwlk 34115 elmrsubrn 34511 ccatcan2d 41069 lswn0 46112

W3C validator