Theorem lencl 14486

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 𝑆 → (♯‘𝑊) ∈ ℕ0)

Proof of Theorem lencl

Step	Hyp	Ref	Expression
1		wrdfin 14485	. 2 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin)
2		hashcl 14309	. 2 ⊢ (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ0)
3	1, 2	syl 17	1 ⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2119  ‘cfv 6485  Fincfn 8883  ℕ₀cn0 12428  ♯chash 14283  Word cword 14466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780  df-fz 13453  df-fzo 13600  df-hash 14284  df-word 14467

This theorem is referenced by:  wrdffz  14488  wrdnfi  14501  wrdsymb0  14502  wrdlenge1n0  14503  wrdlenge2n0  14505  wrdsymb1  14506  eqwrd  14510  wrdred1  14513  wrdred1hash  14514  ccatcl  14527  ccatlen  14528  ccat0  14529  ccatval1  14530  ccatval3  14532  elfzelfzccat  14533  ccatdmss  14535  ccatsymb  14536  ccatfv0  14537  ccatval21sw  14539  ccatlid  14540  ccatrid  14541  ccatass  14542  ccatrn  14543  lswccatn0lsw  14545  ccatalpha  14547  ccatws1lenp1b  14575  wrdlenccats1lenm1  14576  ccatw2s1len  14579  ccats1val2  14581  ccatws1n0  14586  lswccats1fst  14589  ccatw2s1p1  14590  ccat2s1fvw  14592  swrdnd  14608  swrdnd2  14609  swrdnd0  14611  swrdrlen  14613  swrdlen2  14614  swrdfv2  14615  swrdlsw  14621  swrdccat2  14623  pfxid  14638  pfxn0  14640  pfxnd0  14642  addlenpfx  14644  pfxtrcfv0  14647  pfxeq  14649  pfxtrcfvl  14650  pfxsuffeqwrdeq  14651  pfxccat1  14655  pfxcctswrd  14663  ccats1pfxeq  14667  ccats1pfxeqrex  14668  ccatopth2  14670  cats1un  14674  wrdind  14675  wrd2ind  14676  swrdccatin1  14678  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12lem3  14685  pfxccatin12  14686  pfxccat3  14687  swrdccat  14688  pfxccatpfx2  14690  pfxccat3a  14691  swrdccat3blem  14692  swrdccat3b  14693  pfxccatid  14694  ccats1pfxeqbi  14695  spllen  14707  splfv1  14708  splfv2a  14709  splval2  14710  revcl  14714  revlen  14715  revccat  14719  revrev  14720  repswsymball  14732  repswsymballbi  14733  cshw0  14747  cshwsublen  14749  cshwn  14750  cshwlen  14752  cshwidxmod  14756  2cshwid  14767  3cshw  14771  cshweqdif2  14772  cshw1  14775  scshwfzeqfzo  14779  revco  14787  ccatco  14788  cats1fvn  14811  cats1fv  14812  pfx2  14900  swrd2lsw  14905  2swrd2eqwrdeq  14906  ccat2s1fvwALT  14908  cshwshashnsame  17065  chnind  18578  chnub  18579  chnlt  18580  chnccats1  18582  chnccat  18583  chnrev  18584  chnpolleha  18589  chnpolfz  18590  gsmsymgrfixlem1  19393  gsmsymgreqlem2  19397  pmtrdifwrdellem2  19448  psgnuni  19465  psgnran  19481  efginvrel2  19693  efgsdmi  19698  efgsval2  19699  efgsp1  19703  efgsfo  19705  efgredlemf  19707  efgredlemg  19708  efgredleme  19709  efgredlemd  19710  efgredlemc  19711  efgredlem  19713  efgred  19714  efgcpbllemb  19721  frgpuplem  19738  frgpnabllem1  19839  pgpfaclem1  20049  psgnghm  21555  upgrewlkle2  29693  wlkcl  29702  wlkeq  29720  wlkv0  29736  wlklenvclwlk  29740  redwlklem  29756  wlkp1lem3  29760  wlkp1lem8  29765  wlkdlem1  29767  pthdlem1  29852  pthdlem2  29854  wlkiswwlks1  29953  wlkiswwlks2lem1  29955  wlkiswwlks2lem3  29957  wlkiswwlks2lem4  29958  wwlksm1edg  29967  wlklnwwlkln2lem  29968  wwlksnextbi  29980  wwlksnextproplem2  29996  wwlksnextproplem3  29997  rusgrnumwwlks  30063  clwwlkccatlem  30077  umgrclwwlkge2  30079  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a2  30081  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlklem3  30089  clwlkclwwlk  30090  clwlkclwwlk2  30091  clwlkclwwlkfo  30097  clwwisshclwwslem  30102  erclwwlkref  30108  clwwlkn  30114  clwwlkwwlksb  30142  clwlknf1oclwwlknlem1  30169  clwwlknonex2lem2  30196  eupth2eucrct  30305  eucrctshift  30331  numclwlk2lem2f1o  30467  ccatf1  33028  pfxlsw2ccat  33029  ccatws1f1o  33030  ccatws1f1olast  33031  wrdt2ind  33032  splfv3  33037  gsumwrd2dccatlem  33158  gsumwrd2dccat  33159  cycpmfv1  33194  cycpmfv2  33195  cycpmco2f1  33205  cycpmco2rn  33206  cycpmco2lem3  33209  cycpmco2lem4  33210  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2lem7  33213  cycpmco2  33214  cycpmrn  33224  cyc3genpm  33233  1arithidomlem1  33618  1arithidomlem2  33619  1arithidom  33620  dfufd2lem  33632  sseqfv1  34573  sseqfn  34574  sseqmw  34575  sseqf  34576  sseqfv2  34578  sseqp1  34579  ofcccat  34727  signstlen  34751  signstfvn  34753  signstfvp  34755  signstfvneq0  34756  signstfvc  34758  signstfveq0a  34760  signstfveq0  34761  signshf  34772  signshlen  34774  signshnz  34775  lpadlem3  34862  lpadlem2  34864  lpadlen2  34865  lpadmax  34866  lpadleft  34867  lpadright  34868  revpfxsfxrev  35344  revwlk  35353  elmrsubrn  35748  ccatcan2d  42735  chnsubseqword  47323  chnsubseqwl  47324  chnsubseq  47325  chnsuslle  47326  chnerlem1  47327  chnerlem2  47328  lswn0  47919