Theorem lencl 14588

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ‘cfv 6540  Fincfn 8949  ℕ₀cn0 12519  ♯chash 14384  Word cword 14568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191  ax-pre-mulgt0 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-card 9941  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-sub 11458  df-neg 11459  df-nn 12249  df-n0 12520  df-z 12607  df-uz 12879  df-fz 13552  df-fzo 13700  df-hash 14385  df-word 14569

This theorem is used by:  wrdffz  14590  wrdnfi  14603  wrdsymb0  14604  wrdlenge1n0  14605  wrdlenge2n0  14607  wrdsymb1  14608  eqwrd  14612  wrdred1  14615  wrdred1hash  14616  ccatcl  14629  ccatlen  14630  ccat0  14631  ccatval1  14632  ccatval3  14634  elfzelfzccat  14635  ccatdmss  14637  ccatsymb  14638  ccatfv0  14639  ccatval21sw  14641  ccatlid  14642  ccatrid  14643  ccatass  14644  ccatrn  14645  ccatf1  14646  lswccatn0lsw  14648  ccatalpha  14650  ccatws1lenp1b  14679  wrdlenccats1lenm1  14680  ccatw2s1len  14683  ccats1val2  14685  ccatws1n0  14690  lswccats1fst  14693  ccatw2s1p1  14694  ccat2s1fvw  14696  swrdnd  14714  swrdnd2  14715  swrdnd0  14717  swrdrlen  14719  swrdlen2  14720  swrdfv2  14721  swrdlsw  14727  swrdccat2  14729  pfxid  14744  pfxn0  14746  pfxnd0  14748  addlenpfx  14750  pfxtrcfv0  14753  pfxeq  14755  pfxtrcfvl  14756  pfxsuffeqwrdeq  14757  pfxccat1  14761  pfxcctswrd  14769  ccats1pfxeq  14773  ccats1pfxeqrex  14774  ccatopth2  14776  cats1un  14780  wrdind  14781  wrd2ind  14782  swrdccatin1  14784  swrdccatin2  14788  pfxccatin12lem2  14790  pfxccatin12lem3  14791  pfxccatin12  14792  pfxccat3  14793  swrdccat  14794  pfxccatpfx2  14796  pfxccat3a  14797  swrdccat3blem  14798  swrdccat3b  14799  pfxccatid  14800  ccats1pfxeqbi  14801  spllen  14813  splfv1  14814  splfv2a  14815  splval2  14816  revcl  14820  revlen  14821  revccat  14825  revrev  14826  revpfxsfxrev  14827  repswsymball  14840  repswsymballbi  14841  cshw0  14855  cshwsublen  14857  cshwn  14858  cshwlen  14860  cshwidxmod  14864  2cshwid  14875  3cshw  14879  cshweqdif2  14880  cshw1  14883  scshwfzeqfzo  14887  revco  14895  ccatco  14896  cats1fvn  14919  cats1fv  14920  pfx2  15008  swrd2lsw  15013  2swrd2eqwrdeq  15014  ccat2s1fvwALT  15016  cshwshashnsame  17185  chnind  18699  chnub  18700  chnlt  18701  chnccats1  18703  chnccat  18704  chnrev  18705  chnpolleha  18710  chnpolfz  18711  gsmsymgrfixlem1  19541  gsmsymgreqlem2  19545  pmtrdifwrdellem2  19596  psgnuni  19613  psgnran  19629  efginvrel2  19841  efgsdmi  19846  efgsval2  19847  efgsp1  19851  efgsfo  19853  efgredlemf  19855  efgredlemg  19856  efgredleme  19857  efgredlemd  19858  efgredlemc  19859  efgredlem  19861  efgred  19862  efgcpbllemb  19869  frgpuplem  19886  frgpnabllem1  19987  pgpfaclem1  20197  psgnghm  21780  upgrewlkle2  30014  wlkcl  30023  wlkeq  30041  wlkv0  30057  wlklenvclwlk  30061  redwlklem  30077  wlkp1lem3  30081  wlkp1lem8  30086  wlkdlem1  30088  revwlk  30094  pthdlem1  30179  pthdlem2  30181  wlkiswwlks1  30283  wlkiswwlks2lem1  30285  wlkiswwlks2lem3  30287  wlkiswwlks2lem4  30288  wwlksm1edg  30297  wlklnwwlkln2lem  30298  wwlksnextbi  30310  wwlksnextproplem2  30326  wwlksnextproplem3  30327  rusgrnumwwlks  30393  clwwlkccatlem  30407  umgrclwwlkge2  30409  clwlkclwwlklem2a1  30410  clwlkclwwlklem2a2  30411  clwlkclwwlklem2a4  30415  clwlkclwwlklem2a  30416  clwlkclwwlklem2  30418  clwlkclwwlklem3  30419  clwlkclwwlk  30420  clwlkclwwlk2  30421  clwlkclwwlkfo  30427  clwwisshclwwslem  30432  erclwwlkref  30438  clwwlkn  30444  clwwlkwwlksb  30472  clwlknf1oclwwlknlem1  30499  clwwlknonex2lem2  30526  eupth2eucrct  30639  eucrctshift  30665  numclwlk2lem2f1o  30801  pfxlsw2ccat  33336  ccatws1f1o  33337  ccatws1f1olast  33338  wrdt2ind  33339  splfv3  33342  gsumwrd2dccatlem  33461  gsumwrd2dccat  33462  cycpmfv1  33497  cycpmfv2  33498  cycpmco2f1  33508  cycpmco2rn  33509  cycpmco2lem3  33512  cycpmco2lem4  33513  cycpmco2lem5  33514  cycpmco2lem6  33515  cycpmco2lem7  33516  cycpmco2  33517  cycpmrn  33527  cyc3genpm  33536  1arithidomlem1  33889  1arithidomlem2  33890  1arithidom  33891  dfufd2lem  33903  sseqfv1  34844  sseqfn  34845  sseqmw  34846  sseqf  34847  sseqfv2  34849  sseqp1  34850  ofcccat  34998  signstlen  35019  signstfvn  35021  signstfvp  35023  signstfvneq0  35024  signstfvc  35026  signstfveq0a  35028  signstfveq0  35029  signshf  35040  signshlen  35042  signshnz  35043  lpadlem3  35133  lpadlem2  35135  lpadlen2  35136  lpadmax  35137  lpadleft  35138  lpadright  35139  elmrsubrn  36049  ccatcan2d  43077  chnsubseqword  47652  chnsubseqwl  47653  chnsubseq  47654  chnsuslle  47655  chnerlem1  47656  chnerlem2  47657  lswn0  48251