Theorem lencl 14505

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6514  Fincfn 8921  ℕ₀cn0 12449  ♯chash 14302  Word cword 14485

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-card 9899  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537  df-uz 12801  df-fz 13476  df-fzo 13623  df-hash 14303  df-word 14486

This theorem is referenced by:  wrdffz  14507  wrdnfi  14520  wrdsymb0  14521  wrdlenge1n0  14522  wrdlenge2n0  14524  wrdsymb1  14525  eqwrd  14529  wrdred1  14532  wrdred1hash  14533  ccatcl  14546  ccatlen  14547  ccat0  14548  ccatval1  14549  ccatval3  14551  elfzelfzccat  14552  ccatsymb  14554  ccatfv0  14555  ccatval21sw  14557  ccatlid  14558  ccatrid  14559  ccatass  14560  ccatrn  14561  lswccatn0lsw  14563  ccatalpha  14565  ccatws1lenp1b  14593  wrdlenccats1lenm1  14594  ccatw2s1len  14597  ccats1val2  14599  ccatws1n0  14604  lswccats1fst  14607  ccatw2s1p1  14608  ccat2s1fvw  14610  swrdnd  14626  swrdnd2  14627  swrdnd0  14629  swrdrlen  14631  swrdlen2  14632  swrdfv2  14633  swrdlsw  14639  swrdccat2  14641  pfxid  14656  pfxn0  14658  pfxnd0  14660  addlenrevpfx  14662  addlenpfx  14663  pfxtrcfv0  14666  pfxeq  14668  pfxtrcfvl  14669  pfxsuffeqwrdeq  14670  pfxccat1  14674  pfxcctswrd  14682  ccats1pfxeq  14686  ccats1pfxeqrex  14687  ccatopth2  14689  cats1un  14693  wrdind  14694  wrd2ind  14695  swrdccatin1  14697  swrdccatin2  14701  pfxccatin12lem2  14703  pfxccatin12lem3  14704  pfxccatin12  14705  pfxccat3  14706  swrdccat  14707  pfxccatpfx2  14709  pfxccat3a  14710  swrdccat3blem  14711  swrdccat3b  14712  pfxccatid  14713  ccats1pfxeqbi  14714  spllen  14726  splfv1  14727  splfv2a  14728  splval2  14729  revcl  14733  revlen  14734  revccat  14738  revrev  14739  repswsymball  14751  repswsymballbi  14752  cshw0  14766  cshwsublen  14768  cshwn  14769  cshwlen  14771  cshwidxmod  14775  2cshwid  14786  3cshw  14790  cshweqdif2  14791  cshw1  14794  scshwfzeqfzo  14799  revco  14807  ccatco  14808  cats1fvn  14831  cats1fv  14832  pfx2  14920  swrd2lsw  14925  2swrd2eqwrdeq  14926  ccat2s1fvwALT  14928  cshwshashnsame  17081  gsmsymgrfixlem1  19364  gsmsymgreqlem2  19368  pmtrdifwrdellem2  19419  psgnuni  19436  psgnran  19452  efginvrel2  19664  efgsdmi  19669  efgsval2  19670  efgsp1  19674  efgsfo  19676  efgredlemf  19678  efgredlemg  19679  efgredleme  19680  efgredlemd  19681  efgredlemc  19682  efgredlem  19684  efgred  19685  efgcpbllemb  19692  frgpuplem  19709  frgpnabllem1  19810  pgpfaclem1  20020  psgnghm  21496  upgrewlkle2  29541  wlkcl  29550  wlkeq  29569  wlkv0  29586  wlklenvclwlk  29590  redwlklem  29606  wlkp1lem3  29610  wlkp1lem8  29615  wlkdlem1  29617  pthdlem1  29703  pthdlem2  29705  wlkiswwlks1  29804  wlkiswwlks2lem1  29806  wlkiswwlks2lem3  29808  wlkiswwlks2lem4  29809  wwlksm1edg  29818  wlklnwwlkln2lem  29819  wwlksnextbi  29831  wwlksnextproplem2  29847  wwlksnextproplem3  29848  rusgrnumwwlks  29911  clwwlkccatlem  29925  umgrclwwlkge2  29927  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a2  29929  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlklem3  29937  clwlkclwwlk  29938  clwlkclwwlk2  29939  clwlkclwwlkfo  29945  clwwisshclwwslem  29950  erclwwlkref  29956  clwwlkn  29962  clwwlkwwlksb  29990  clwlknf1oclwwlknlem1  30017  clwwlknonex2lem2  30044  eupth2eucrct  30153  eucrctshift  30179  numclwlk2lem2f1o  30315  ccatf1  32877  ccatdmss  32878  pfxlsw2ccat  32879  ccatws1f1o  32880  ccatws1f1olast  32881  wrdt2ind  32882  splfv3  32887  chnind  32944  chnub  32945  chnlt  32946  chnccats1  32948  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  cycpmfv1  33077  cycpmfv2  33078  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  cycpmrn  33107  cyc3genpm  33116  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  dfufd2lem  33527  sseqfv1  34387  sseqfn  34388  sseqmw  34389  sseqf  34390  sseqfv2  34392  sseqp1  34393  ofcccat  34541  signstlen  34565  signstfvn  34567  signstfvp  34569  signstfvneq0  34570  signstfvc  34572  signstfveq0a  34574  signstfveq0  34575  signshf  34586  signshlen  34588  signshnz  34589  lpadlem3  34676  lpadlem2  34678  lpadlen2  34679  lpadmax  34680  lpadleft  34681  lpadright  34682  revpfxsfxrev  35110  revwlk  35119  elmrsubrn  35514  ccatcan2d  42246  lswn0  47449