Theorem lencl 13883

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6355  Fincfn 8509  ℕ₀cn0 11898  ♯chash 13691  Word cword 13862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-oadd 8106  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-card 9368  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-n0 11899  df-z 11983  df-uz 12245  df-fz 12894  df-fzo 13035  df-hash 13692  df-word 13863

This theorem is referenced by:  wrdffz  13885  wrdnfi  13899  wrdsymb0  13901  wrdlenge1n0  13902  wrdlenge2n0  13904  wrdsymb1  13905  eqwrd  13909  wrdred1  13912  wrdred1hash  13913  ccatcl  13926  ccatlen  13927  ccatlenOLD  13928  ccat0  13929  ccatval1  13930  ccatval1OLD  13931  ccatval3  13933  elfzelfzccat  13934  ccatsymb  13936  ccatfv0  13937  ccatval21sw  13939  ccatlid  13940  ccatrid  13941  ccatass  13942  ccatrn  13943  lswccatn0lsw  13945  ccatalpha  13947  ccatws1lenp1b  13975  wrdlenccats1lenm1  13976  ccatw2s1len  13980  ccats1val2  13983  ccatws1n0  13991  lswccats1fst  13994  ccatw2s1p1  13995  ccatw2s1p1OLD  13996  ccat2s1fvw  13998  ccat2s1fvwOLD  13999  swrdnd  14016  swrdnd2  14017  swrdnd0  14019  swrdrlen  14021  swrdlen2  14022  swrdfv2  14023  swrdlsw  14029  swrdccat2  14031  pfxid  14046  pfxn0  14048  pfxnd0  14050  addlenrevpfx  14052  addlenpfx  14053  pfxtrcfv0  14056  pfxeq  14058  pfxtrcfvl  14059  pfxsuffeqwrdeq  14060  pfxccat1  14064  pfxcctswrd  14072  ccats1pfxeq  14076  ccats1pfxeqrex  14077  ccatopth2  14079  cats1un  14083  wrdind  14084  wrd2ind  14085  swrdccatin1  14087  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12lem3  14094  pfxccatin12  14095  pfxccat3  14096  swrdccat  14097  pfxccatpfx2  14099  pfxccat3a  14100  swrdccat3blem  14101  swrdccat3b  14102  pfxccatid  14103  ccats1pfxeqbi  14104  spllen  14116  splfv1  14117  splfv2a  14118  splval2  14119  revcl  14123  revlen  14124  revccat  14128  revrev  14129  repswsymball  14141  repswsymballbi  14142  cshw0  14156  cshwsublen  14158  cshwn  14159  cshwlen  14161  cshwidxmod  14165  2cshwid  14176  3cshw  14180  cshweqdif2  14181  cshw1  14184  scshwfzeqfzo  14188  revco  14196  ccatco  14197  cats1fvn  14220  cats1fv  14221  pfx2  14309  swrd2lsw  14314  2swrd2eqwrdeq  14315  ccat2s1fvwALT  14318  ccat2s1fvwALTOLD  14319  cshwshashnsame  16437  gsmsymgrfixlem1  18555  gsmsymgreqlem2  18559  pmtrdifwrdellem2  18610  psgnuni  18627  psgnran  18643  efginvrel2  18853  efgsdmi  18858  efgsval2  18859  efgsp1  18863  efgsfo  18865  efgredlemf  18867  efgredlemg  18868  efgredleme  18869  efgredlemd  18870  efgredlemc  18871  efgredlem  18873  efgred  18874  efgcpbllemb  18881  frgpuplem  18898  frgpnabllem1  18993  pgpfaclem1  19203  psgnghm  20724  upgrewlkle2  27388  wlkcl  27397  wlkeq  27415  wlkv0  27432  wlklenvclwlk  27436  wlklenvclwlkOLD  27437  redwlklem  27453  wlkp1lem3  27457  wlkp1lem8  27462  wlkdlem1  27464  pthdlem1  27547  pthdlem2  27549  wlkiswwlks1  27645  wlkiswwlks2lem1  27647  wlkiswwlks2lem3  27649  wlkiswwlks2lem4  27650  wwlksm1edg  27659  wlklnwwlkln2lem  27660  wwlksnextbi  27672  wwlksnextproplem2  27689  wwlksnextproplem3  27690  rusgrnumwwlks  27753  clwwlkccatlem  27767  umgrclwwlkge2  27769  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a2  27771  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlklem3  27779  clwlkclwwlk  27780  clwlkclwwlk2  27781  clwlkclwwlkfo  27787  clwwisshclwwslem  27792  erclwwlkref  27798  clwwlkn  27804  clwwlkwwlksb  27833  clwlknf1oclwwlknlem1  27860  clwwlknonex2lem2  27887  eupth2eucrct  27996  eucrctshift  28022  numclwlk2lem2f1o  28158  ccatf1  30625  pfxlsw2ccat  30626  wrdt2ind  30627  splfv3  30632  cycpmfv1  30755  cycpmfv2  30756  cycpmco2f1  30766  cycpmco2rn  30767  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  cycpmrn  30785  cyc3genpm  30794  sseqfv1  31647  sseqfn  31648  sseqmw  31649  sseqf  31650  sseqfv2  31652  sseqp1  31653  ofcccat  31813  signstlen  31837  signstfvn  31839  signstfvp  31841  signstfvneq0  31842  signstfvc  31844  signstfveq0a  31846  signstfveq0  31847  signshf  31858  signshlen  31860  signshnz  31861  lpadlem3  31949  lpadlem2  31951  lpadlen2  31952  lpadmax  31953  lpadleft  31954  lpadright  31955  revpfxsfxrev  32362  revwlk  32371  elmrsubrn  32767  ccatcan2d  39147  lswn0  43624