Theorem lencl 14479

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6540  Fincfn 8935  ℕ₀cn0 12468  ♯chash 14286  Word cword 14460

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-fzo 13624  df-hash 14287  df-word 14461

This theorem is referenced by:  wrdffz  14481  wrdnfi  14494  wrdsymb0  14495  wrdlenge1n0  14496  wrdlenge2n0  14498  wrdsymb1  14499  eqwrd  14503  wrdred1  14506  wrdred1hash  14507  ccatcl  14520  ccatlen  14521  ccat0  14522  ccatval1  14523  ccatval3  14525  elfzelfzccat  14526  ccatsymb  14528  ccatfv0  14529  ccatval21sw  14531  ccatlid  14532  ccatrid  14533  ccatass  14534  ccatrn  14535  lswccatn0lsw  14537  ccatalpha  14539  ccatws1lenp1b  14567  wrdlenccats1lenm1  14568  ccatw2s1len  14571  ccats1val2  14573  ccatws1n0  14578  lswccats1fst  14581  ccatw2s1p1  14582  ccat2s1fvw  14584  swrdnd  14600  swrdnd2  14601  swrdnd0  14603  swrdrlen  14605  swrdlen2  14606  swrdfv2  14607  swrdlsw  14613  swrdccat2  14615  pfxid  14630  pfxn0  14632  pfxnd0  14634  addlenrevpfx  14636  addlenpfx  14637  pfxtrcfv0  14640  pfxeq  14642  pfxtrcfvl  14643  pfxsuffeqwrdeq  14644  pfxccat1  14648  pfxcctswrd  14656  ccats1pfxeq  14660  ccats1pfxeqrex  14661  ccatopth2  14663  cats1un  14667  wrdind  14668  wrd2ind  14669  swrdccatin1  14671  swrdccatin2  14675  pfxccatin12lem2  14677  pfxccatin12lem3  14678  pfxccatin12  14679  pfxccat3  14680  swrdccat  14681  pfxccatpfx2  14683  pfxccat3a  14684  swrdccat3blem  14685  swrdccat3b  14686  pfxccatid  14687  ccats1pfxeqbi  14688  spllen  14700  splfv1  14701  splfv2a  14702  splval2  14703  revcl  14707  revlen  14708  revccat  14712  revrev  14713  repswsymball  14725  repswsymballbi  14726  cshw0  14740  cshwsublen  14742  cshwn  14743  cshwlen  14745  cshwidxmod  14749  2cshwid  14760  3cshw  14764  cshweqdif2  14765  cshw1  14768  scshwfzeqfzo  14773  revco  14781  ccatco  14782  cats1fvn  14805  cats1fv  14806  pfx2  14894  swrd2lsw  14899  2swrd2eqwrdeq  14900  ccat2s1fvwALT  14902  cshwshashnsame  17033  gsmsymgrfixlem1  19289  gsmsymgreqlem2  19293  pmtrdifwrdellem2  19344  psgnuni  19361  psgnran  19377  efginvrel2  19589  efgsdmi  19594  efgsval2  19595  efgsp1  19599  efgsfo  19601  efgredlemf  19603  efgredlemg  19604  efgredleme  19605  efgredlemd  19606  efgredlemc  19607  efgredlem  19609  efgred  19610  efgcpbllemb  19617  frgpuplem  19634  frgpnabllem1  19735  pgpfaclem1  19945  psgnghm  21124  upgrewlkle2  28852  wlkcl  28861  wlkeq  28880  wlkv0  28897  wlklenvclwlk  28901  redwlklem  28917  wlkp1lem3  28921  wlkp1lem8  28926  wlkdlem1  28928  pthdlem1  29012  pthdlem2  29014  wlkiswwlks1  29110  wlkiswwlks2lem1  29112  wlkiswwlks2lem3  29114  wlkiswwlks2lem4  29115  wwlksm1edg  29124  wlklnwwlkln2lem  29125  wwlksnextbi  29137  wwlksnextproplem2  29153  wwlksnextproplem3  29154  rusgrnumwwlks  29217  clwwlkccatlem  29231  umgrclwwlkge2  29233  clwlkclwwlklem2a1  29234  clwlkclwwlklem2a2  29235  clwlkclwwlklem2a4  29239  clwlkclwwlklem2a  29240  clwlkclwwlklem2  29242  clwlkclwwlklem3  29243  clwlkclwwlk  29244  clwlkclwwlk2  29245  clwlkclwwlkfo  29251  clwwisshclwwslem  29256  erclwwlkref  29262  clwwlkn  29268  clwwlkwwlksb  29296  clwlknf1oclwwlknlem1  29323  clwwlknonex2lem2  29350  eupth2eucrct  29459  eucrctshift  29485  numclwlk2lem2f1o  29621  ccatf1  32102  pfxlsw2ccat  32103  wrdt2ind  32104  splfv3  32109  cycpmfv1  32259  cycpmfv2  32260  cycpmco2f1  32270  cycpmco2rn  32271  cycpmco2lem3  32274  cycpmco2lem4  32275  cycpmco2lem5  32276  cycpmco2lem6  32277  cycpmco2lem7  32278  cycpmco2  32279  cycpmrn  32289  cyc3genpm  32298  sseqfv1  33376  sseqfn  33377  sseqmw  33378  sseqf  33379  sseqfv2  33381  sseqp1  33382  ofcccat  33542  signstlen  33566  signstfvn  33568  signstfvp  33570  signstfvneq0  33571  signstfvc  33573  signstfveq0a  33575  signstfveq0  33576  signshf  33587  signshlen  33589  signshnz  33590  lpadlem3  33678  lpadlem2  33680  lpadlen2  33681  lpadmax  33682  lpadleft  33683  lpadright  33684  revpfxsfxrev  34094  revwlk  34103  elmrsubrn  34499  ccatcan2d  41066  lswn0  46098