Theorem lencl 14489

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 14488	. 2 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin)
2		hashcl 14312	. 2 ⊢ (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ0)
3	1, 2	syl 17	1 ⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6493  Fincfn 8887  ℕ₀cn0 12431  ♯chash 14286  Word cword 14469

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-card 9857  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432  df-z 12519  df-uz 12783  df-fz 13456  df-fzo 13603  df-hash 14287  df-word 14470

This theorem is referenced by:  wrdffz  14491  wrdnfi  14504  wrdsymb0  14505  wrdlenge1n0  14506  wrdlenge2n0  14508  wrdsymb1  14509  eqwrd  14513  wrdred1  14516  wrdred1hash  14517  ccatcl  14530  ccatlen  14531  ccat0  14532  ccatval1  14533  ccatval3  14535  elfzelfzccat  14536  ccatdmss  14538  ccatsymb  14539  ccatfv0  14540  ccatval21sw  14542  ccatlid  14543  ccatrid  14544  ccatass  14545  ccatrn  14546  lswccatn0lsw  14548  ccatalpha  14550  ccatws1lenp1b  14578  wrdlenccats1lenm1  14579  ccatw2s1len  14582  ccats1val2  14584  ccatws1n0  14589  lswccats1fst  14592  ccatw2s1p1  14593  ccat2s1fvw  14595  swrdnd  14611  swrdnd2  14612  swrdnd0  14614  swrdrlen  14616  swrdlen2  14617  swrdfv2  14618  swrdlsw  14624  swrdccat2  14626  pfxid  14641  pfxn0  14643  pfxnd0  14645  addlenpfx  14647  pfxtrcfv0  14650  pfxeq  14652  pfxtrcfvl  14653  pfxsuffeqwrdeq  14654  pfxccat1  14658  pfxcctswrd  14666  ccats1pfxeq  14670  ccats1pfxeqrex  14671  ccatopth2  14673  cats1un  14677  wrdind  14678  wrd2ind  14679  swrdccatin1  14681  swrdccatin2  14685  pfxccatin12lem2  14687  pfxccatin12lem3  14688  pfxccatin12  14689  pfxccat3  14690  swrdccat  14691  pfxccatpfx2  14693  pfxccat3a  14694  swrdccat3blem  14695  swrdccat3b  14696  pfxccatid  14697  ccats1pfxeqbi  14698  spllen  14710  splfv1  14711  splfv2a  14712  splval2  14713  revcl  14717  revlen  14718  revccat  14722  revrev  14723  repswsymball  14735  repswsymballbi  14736  cshw0  14750  cshwsublen  14752  cshwn  14753  cshwlen  14755  cshwidxmod  14759  2cshwid  14770  3cshw  14774  cshweqdif2  14775  cshw1  14778  scshwfzeqfzo  14782  revco  14790  ccatco  14791  cats1fvn  14814  cats1fv  14815  pfx2  14903  swrd2lsw  14908  2swrd2eqwrdeq  14909  ccat2s1fvwALT  14911  cshwshashnsame  17068  chnind  18581  chnub  18582  chnlt  18583  chnccats1  18585  chnccat  18586  chnrev  18587  chnpolleha  18592  chnpolfz  18593  gsmsymgrfixlem1  19396  gsmsymgreqlem2  19400  pmtrdifwrdellem2  19451  psgnuni  19468  psgnran  19484  efginvrel2  19696  efgsdmi  19701  efgsval2  19702  efgsp1  19706  efgsfo  19708  efgredlemf  19710  efgredlemg  19711  efgredleme  19712  efgredlemd  19713  efgredlemc  19714  efgredlem  19716  efgred  19717  efgcpbllemb  19724  frgpuplem  19741  frgpnabllem1  19842  pgpfaclem1  20052  psgnghm  21573  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  33027  pfxlsw2ccat  33028  ccatws1f1o  33029  ccatws1f1olast  33030  wrdt2ind  33031  splfv3  33036  gsumwrd2dccatlem  33156  gsumwrd2dccat  33157  cycpmfv1  33192  cycpmfv2  33193  cycpmco2f1  33203  cycpmco2rn  33204  cycpmco2lem3  33207  cycpmco2lem4  33208  cycpmco2lem5  33209  cycpmco2lem6  33210  cycpmco2lem7  33211  cycpmco2  33212  cycpmrn  33222  cyc3genpm  33231  1arithidomlem1  33613  1arithidomlem2  33614  1arithidom  33615  dfufd2lem  33627  sseqfv1  34552  sseqfn  34553  sseqmw  34554  sseqf  34555  sseqfv2  34557  sseqp1  34558  ofcccat  34706  signstlen  34730  signstfvn  34732  signstfvp  34734  signstfvneq0  34735  signstfvc  34737  signstfveq0a  34739  signstfveq0  34740  signshf  34751  signshlen  34753  signshnz  34754  lpadlem3  34841  lpadlem2  34843  lpadlen2  34844  lpadmax  34845  lpadleft  34846  lpadright  34847  revpfxsfxrev  35317  revwlk  35326  elmrsubrn  35721  ccatcan2d  42707  chnsubseqword  47327  chnsubseqwl  47328  chnsubseq  47329  chnsuslle  47330  chnerlem1  47331  chnerlem2  47332  lswn0  47919