Theorem lencl 14567

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6562  Fincfn 8983  ℕ₀cn0 12523  ♯chash 14365  Word cword 14548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-n0 12524  df-z 12611  df-uz 12876  df-fz 13544  df-fzo 13691  df-hash 14366  df-word 14549

This theorem is referenced by:  wrdffz  14569  wrdnfi  14582  wrdsymb0  14583  wrdlenge1n0  14584  wrdlenge2n0  14586  wrdsymb1  14587  eqwrd  14591  wrdred1  14594  wrdred1hash  14595  ccatcl  14608  ccatlen  14609  ccat0  14610  ccatval1  14611  ccatval3  14613  elfzelfzccat  14614  ccatsymb  14616  ccatfv0  14617  ccatval21sw  14619  ccatlid  14620  ccatrid  14621  ccatass  14622  ccatrn  14623  lswccatn0lsw  14625  ccatalpha  14627  ccatws1lenp1b  14655  wrdlenccats1lenm1  14656  ccatw2s1len  14659  ccats1val2  14661  ccatws1n0  14666  lswccats1fst  14669  ccatw2s1p1  14670  ccat2s1fvw  14672  swrdnd  14688  swrdnd2  14689  swrdnd0  14691  swrdrlen  14693  swrdlen2  14694  swrdfv2  14695  swrdlsw  14701  swrdccat2  14703  pfxid  14718  pfxn0  14720  pfxnd0  14722  addlenrevpfx  14724  addlenpfx  14725  pfxtrcfv0  14728  pfxeq  14730  pfxtrcfvl  14731  pfxsuffeqwrdeq  14732  pfxccat1  14736  pfxcctswrd  14744  ccats1pfxeq  14748  ccats1pfxeqrex  14749  ccatopth2  14751  cats1un  14755  wrdind  14756  wrd2ind  14757  swrdccatin1  14759  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12lem3  14766  pfxccatin12  14767  pfxccat3  14768  swrdccat  14769  pfxccatpfx2  14771  pfxccat3a  14772  swrdccat3blem  14773  swrdccat3b  14774  pfxccatid  14775  ccats1pfxeqbi  14776  spllen  14788  splfv1  14789  splfv2a  14790  splval2  14791  revcl  14795  revlen  14796  revccat  14800  revrev  14801  repswsymball  14813  repswsymballbi  14814  cshw0  14828  cshwsublen  14830  cshwn  14831  cshwlen  14833  cshwidxmod  14837  2cshwid  14848  3cshw  14852  cshweqdif2  14853  cshw1  14856  scshwfzeqfzo  14861  revco  14869  ccatco  14870  cats1fvn  14893  cats1fv  14894  pfx2  14982  swrd2lsw  14987  2swrd2eqwrdeq  14988  ccat2s1fvwALT  14990  cshwshashnsame  17137  gsmsymgrfixlem1  19459  gsmsymgreqlem2  19463  pmtrdifwrdellem2  19514  psgnuni  19531  psgnran  19547  efginvrel2  19759  efgsdmi  19764  efgsval2  19765  efgsp1  19769  efgsfo  19771  efgredlemf  19773  efgredlemg  19774  efgredleme  19775  efgredlemd  19776  efgredlemc  19777  efgredlem  19779  efgred  19780  efgcpbllemb  19787  frgpuplem  19804  frgpnabllem1  19905  pgpfaclem1  20115  psgnghm  21615  upgrewlkle2  29638  wlkcl  29647  wlkeq  29666  wlkv0  29683  wlklenvclwlk  29687  redwlklem  29703  wlkp1lem3  29707  wlkp1lem8  29712  wlkdlem1  29714  pthdlem1  29798  pthdlem2  29800  wlkiswwlks1  29896  wlkiswwlks2lem1  29898  wlkiswwlks2lem3  29900  wlkiswwlks2lem4  29901  wwlksm1edg  29910  wlklnwwlkln2lem  29911  wwlksnextbi  29923  wwlksnextproplem2  29939  wwlksnextproplem3  29940  rusgrnumwwlks  30003  clwwlkccatlem  30017  umgrclwwlkge2  30019  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a2  30021  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlklem3  30029  clwlkclwwlk  30030  clwlkclwwlk2  30031  clwlkclwwlkfo  30037  clwwisshclwwslem  30042  erclwwlkref  30048  clwwlkn  30054  clwwlkwwlksb  30082  clwlknf1oclwwlknlem1  30109  clwwlknonex2lem2  30136  eupth2eucrct  30245  eucrctshift  30271  numclwlk2lem2f1o  30407  ccatf1  32917  ccatdmss  32918  pfxlsw2ccat  32919  ccatws1f1o  32920  ccatws1f1olast  32921  wrdt2ind  32922  splfv3  32927  chnind  32984  chnub  32985  chnlt  32986  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  cycpmfv1  33115  cycpmfv2  33116  cycpmco2f1  33126  cycpmco2rn  33127  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  cycpmrn  33145  cyc3genpm  33154  1arithidomlem1  33542  1arithidomlem2  33543  1arithidom  33544  dfufd2lem  33556  sseqfv1  34370  sseqfn  34371  sseqmw  34372  sseqf  34373  sseqfv2  34375  sseqp1  34376  ofcccat  34536  signstlen  34560  signstfvn  34562  signstfvp  34564  signstfvneq0  34565  signstfvc  34567  signstfveq0a  34569  signstfveq0  34570  signshf  34581  signshlen  34583  signshnz  34584  lpadlem3  34671  lpadlem2  34673  lpadlen2  34674  lpadmax  34675  lpadleft  34676  lpadright  34677  revpfxsfxrev  35099  revwlk  35108  elmrsubrn  35504  ccatcan2d  42270  lswn0  47368