Theorem lencl 14457

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6490  Fincfn 8884  ℕ₀cn0 12402  ♯chash 14254  Word cword 14437

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 5212  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104

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 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-1o 8396  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-card 9852  df-pnf 11169  df-mnf 11170  df-xr 11171  df-ltxr 11172  df-le 11173  df-sub 11367  df-neg 11368  df-nn 12147  df-n0 12403  df-z 12490  df-uz 12753  df-fz 13425  df-fzo 13572  df-hash 14255  df-word 14438

This theorem is referenced by:  wrdffz  14459  wrdnfi  14472  wrdsymb0  14473  wrdlenge1n0  14474  wrdlenge2n0  14476  wrdsymb1  14477  eqwrd  14481  wrdred1  14484  wrdred1hash  14485  ccatcl  14498  ccatlen  14499  ccat0  14500  ccatval1  14501  ccatval3  14503  elfzelfzccat  14504  ccatdmss  14506  ccatsymb  14507  ccatfv0  14508  ccatval21sw  14510  ccatlid  14511  ccatrid  14512  ccatass  14513  ccatrn  14514  lswccatn0lsw  14516  ccatalpha  14518  ccatws1lenp1b  14546  wrdlenccats1lenm1  14547  ccatw2s1len  14550  ccats1val2  14552  ccatws1n0  14557  lswccats1fst  14560  ccatw2s1p1  14561  ccat2s1fvw  14563  swrdnd  14579  swrdnd2  14580  swrdnd0  14582  swrdrlen  14584  swrdlen2  14585  swrdfv2  14586  swrdlsw  14592  swrdccat2  14594  pfxid  14609  pfxn0  14611  pfxnd0  14613  addlenpfx  14615  pfxtrcfv0  14618  pfxeq  14620  pfxtrcfvl  14621  pfxsuffeqwrdeq  14622  pfxccat1  14626  pfxcctswrd  14634  ccats1pfxeq  14638  ccats1pfxeqrex  14639  ccatopth2  14641  cats1un  14645  wrdind  14646  wrd2ind  14647  swrdccatin1  14649  swrdccatin2  14653  pfxccatin12lem2  14655  pfxccatin12lem3  14656  pfxccatin12  14657  pfxccat3  14658  swrdccat  14659  pfxccatpfx2  14661  pfxccat3a  14662  swrdccat3blem  14663  swrdccat3b  14664  pfxccatid  14665  ccats1pfxeqbi  14666  spllen  14678  splfv1  14679  splfv2a  14680  splval2  14681  revcl  14685  revlen  14686  revccat  14690  revrev  14691  repswsymball  14703  repswsymballbi  14704  cshw0  14718  cshwsublen  14720  cshwn  14721  cshwlen  14723  cshwidxmod  14727  2cshwid  14738  3cshw  14742  cshweqdif2  14743  cshw1  14746  scshwfzeqfzo  14750  revco  14758  ccatco  14759  cats1fvn  14782  cats1fv  14783  pfx2  14871  swrd2lsw  14876  2swrd2eqwrdeq  14877  ccat2s1fvwALT  14879  cshwshashnsame  17032  chnind  18545  chnub  18546  chnlt  18547  chnccats1  18549  chnccat  18550  chnrev  18551  chnpolleha  18556  chnpolfz  18557  gsmsymgrfixlem1  19360  gsmsymgreqlem2  19364  pmtrdifwrdellem2  19415  psgnuni  19432  psgnran  19448  efginvrel2  19660  efgsdmi  19665  efgsval2  19666  efgsp1  19670  efgsfo  19672  efgredlemf  19674  efgredlemg  19675  efgredleme  19676  efgredlemd  19677  efgredlemc  19678  efgredlem  19680  efgred  19681  efgcpbllemb  19688  frgpuplem  19705  frgpnabllem1  19806  pgpfaclem1  20016  psgnghm  21537  upgrewlkle2  29664  wlkcl  29673  wlkeq  29691  wlkv0  29707  wlklenvclwlk  29711  redwlklem  29727  wlkp1lem3  29731  wlkp1lem8  29736  wlkdlem1  29738  pthdlem1  29823  pthdlem2  29825  wlkiswwlks1  29924  wlkiswwlks2lem1  29926  wlkiswwlks2lem3  29928  wlkiswwlks2lem4  29929  wwlksm1edg  29938  wlklnwwlkln2lem  29939  wwlksnextbi  29951  wwlksnextproplem2  29967  wwlksnextproplem3  29968  rusgrnumwwlks  30034  clwwlkccatlem  30048  umgrclwwlkge2  30050  clwlkclwwlklem2a1  30051  clwlkclwwlklem2a2  30052  clwlkclwwlklem2a4  30056  clwlkclwwlklem2a  30057  clwlkclwwlklem2  30059  clwlkclwwlklem3  30060  clwlkclwwlk  30061  clwlkclwwlk2  30062  clwlkclwwlkfo  30068  clwwisshclwwslem  30073  erclwwlkref  30079  clwwlkn  30085  clwwlkwwlksb  30113  clwlknf1oclwwlknlem1  30140  clwwlknonex2lem2  30167  eupth2eucrct  30276  eucrctshift  30302  numclwlk2lem2f1o  30438  ccatf1  33014  pfxlsw2ccat  33015  ccatws1f1o  33016  ccatws1f1olast  33017  wrdt2ind  33018  splfv3  33023  gsumwrd2dccatlem  33143  gsumwrd2dccat  33144  cycpmfv1  33179  cycpmfv2  33180  cycpmco2f1  33190  cycpmco2rn  33191  cycpmco2lem3  33194  cycpmco2lem4  33195  cycpmco2lem5  33196  cycpmco2lem6  33197  cycpmco2lem7  33198  cycpmco2  33199  cycpmrn  33209  cyc3genpm  33218  1arithidomlem1  33600  1arithidomlem2  33601  1arithidom  33602  dfufd2lem  33614  sseqfv1  34539  sseqfn  34540  sseqmw  34541  sseqf  34542  sseqfv2  34544  sseqp1  34545  ofcccat  34693  signstlen  34717  signstfvn  34719  signstfvp  34721  signstfvneq0  34722  signstfvc  34724  signstfveq0a  34726  signstfveq0  34727  signshf  34738  signshlen  34740  signshnz  34741  lpadlem3  34828  lpadlem2  34830  lpadlen2  34831  lpadmax  34832  lpadleft  34833  lpadright  34834  revpfxsfxrev  35304  revwlk  35313  elmrsubrn  35708  ccatcan2d  42682  chnsubseqword  47310  chnsubseqwl  47311  chnsubseq  47312  chnsuslle  47313  chnerlem1  47314  chnerlem2  47315  lswn0  47878