Theorem lencl 14164

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  Fincfn 8691  ℕ₀cn0 12163  ♯chash 13972  Word cword 14145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-card 9628  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250  df-uz 12512  df-fz 13169  df-fzo 13312  df-hash 13973  df-word 14146

This theorem is referenced by:  wrdffz  14166  wrdnfi  14179  wrdsymb0  14180  wrdlenge1n0  14181  wrdlenge2n0  14183  wrdsymb1  14184  eqwrd  14188  wrdred1  14191  wrdred1hash  14192  ccatcl  14205  ccatlen  14206  ccatlenOLD  14207  ccat0  14208  ccatval1  14209  ccatval1OLD  14210  ccatval3  14212  elfzelfzccat  14213  ccatsymb  14215  ccatfv0  14216  ccatval21sw  14218  ccatlid  14219  ccatrid  14220  ccatass  14221  ccatrn  14222  lswccatn0lsw  14224  ccatalpha  14226  ccatws1lenp1b  14254  wrdlenccats1lenm1  14255  ccatw2s1len  14259  ccats1val2  14262  ccatws1n0  14270  lswccats1fst  14273  ccatw2s1p1  14274  ccatw2s1p1OLD  14275  ccat2s1fvw  14277  ccat2s1fvwOLD  14278  swrdnd  14295  swrdnd2  14296  swrdnd0  14298  swrdrlen  14300  swrdlen2  14301  swrdfv2  14302  swrdlsw  14308  swrdccat2  14310  pfxid  14325  pfxn0  14327  pfxnd0  14329  addlenrevpfx  14331  addlenpfx  14332  pfxtrcfv0  14335  pfxeq  14337  pfxtrcfvl  14338  pfxsuffeqwrdeq  14339  pfxccat1  14343  pfxcctswrd  14351  ccats1pfxeq  14355  ccats1pfxeqrex  14356  ccatopth2  14358  cats1un  14362  wrdind  14363  wrd2ind  14364  swrdccatin1  14366  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12lem3  14373  pfxccatin12  14374  pfxccat3  14375  swrdccat  14376  pfxccatpfx2  14378  pfxccat3a  14379  swrdccat3blem  14380  swrdccat3b  14381  pfxccatid  14382  ccats1pfxeqbi  14383  spllen  14395  splfv1  14396  splfv2a  14397  splval2  14398  revcl  14402  revlen  14403  revccat  14407  revrev  14408  repswsymball  14420  repswsymballbi  14421  cshw0  14435  cshwsublen  14437  cshwn  14438  cshwlen  14440  cshwidxmod  14444  2cshwid  14455  3cshw  14459  cshweqdif2  14460  cshw1  14463  scshwfzeqfzo  14467  revco  14475  ccatco  14476  cats1fvn  14499  cats1fv  14500  pfx2  14588  swrd2lsw  14593  2swrd2eqwrdeq  14594  ccat2s1fvwALT  14597  ccat2s1fvwALTOLD  14598  cshwshashnsame  16733  gsmsymgrfixlem1  18950  gsmsymgreqlem2  18954  pmtrdifwrdellem2  19005  psgnuni  19022  psgnran  19038  efginvrel2  19248  efgsdmi  19253  efgsval2  19254  efgsp1  19258  efgsfo  19260  efgredlemf  19262  efgredlemg  19263  efgredleme  19264  efgredlemd  19265  efgredlemc  19266  efgredlem  19268  efgred  19269  efgcpbllemb  19276  frgpuplem  19293  frgpnabllem1  19389  pgpfaclem1  19599  psgnghm  20697  upgrewlkle2  27876  wlkcl  27885  wlkeq  27903  wlkv0  27920  wlklenvclwlk  27924  wlklenvclwlkOLD  27925  redwlklem  27941  wlkp1lem3  27945  wlkp1lem8  27950  wlkdlem1  27952  pthdlem1  28035  pthdlem2  28037  wlkiswwlks1  28133  wlkiswwlks2lem1  28135  wlkiswwlks2lem3  28137  wlkiswwlks2lem4  28138  wwlksm1edg  28147  wlklnwwlkln2lem  28148  wwlksnextbi  28160  wwlksnextproplem2  28176  wwlksnextproplem3  28177  rusgrnumwwlks  28240  clwwlkccatlem  28254  umgrclwwlkge2  28256  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a2  28258  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwlkclwwlklem3  28266  clwlkclwwlk  28267  clwlkclwwlk2  28268  clwlkclwwlkfo  28274  clwwisshclwwslem  28279  erclwwlkref  28285  clwwlkn  28291  clwwlkwwlksb  28319  clwlknf1oclwwlknlem1  28346  clwwlknonex2lem2  28373  eupth2eucrct  28482  eucrctshift  28508  numclwlk2lem2f1o  28644  ccatf1  31125  pfxlsw2ccat  31126  wrdt2ind  31127  splfv3  31132  cycpmfv1  31282  cycpmfv2  31283  cycpmco2f1  31293  cycpmco2rn  31294  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  cycpmrn  31312  cyc3genpm  31321  sseqfv1  32256  sseqfn  32257  sseqmw  32258  sseqf  32259  sseqfv2  32261  sseqp1  32262  ofcccat  32422  signstlen  32446  signstfvn  32448  signstfvp  32450  signstfvneq0  32451  signstfvc  32453  signstfveq0a  32455  signstfveq0  32456  signshf  32467  signshlen  32469  signshnz  32470  lpadlem3  32558  lpadlem2  32560  lpadlen2  32561  lpadmax  32562  lpadleft  32563  lpadright  32564  revpfxsfxrev  32977  revwlk  32986  elmrsubrn  33382  ccatcan2d  40145  lswn0  44784