Theorem lencl 14495

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6498  Fincfn 8893  ℕ₀cn0 12437  ♯chash 14292  Word cword 14475

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 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525  df-uz 12789  df-fz 13462  df-fzo 13609  df-hash 14293  df-word 14476

This theorem is referenced by:  wrdffz  14497  wrdnfi  14510  wrdsymb0  14511  wrdlenge1n0  14512  wrdlenge2n0  14514  wrdsymb1  14515  eqwrd  14519  wrdred1  14522  wrdred1hash  14523  ccatcl  14536  ccatlen  14537  ccat0  14538  ccatval1  14539  ccatval3  14541  elfzelfzccat  14542  ccatdmss  14544  ccatsymb  14545  ccatfv0  14546  ccatval21sw  14548  ccatlid  14549  ccatrid  14550  ccatass  14551  ccatrn  14552  lswccatn0lsw  14554  ccatalpha  14556  ccatws1lenp1b  14584  wrdlenccats1lenm1  14585  ccatw2s1len  14588  ccats1val2  14590  ccatws1n0  14595  lswccats1fst  14598  ccatw2s1p1  14599  ccat2s1fvw  14601  swrdnd  14617  swrdnd2  14618  swrdnd0  14620  swrdrlen  14622  swrdlen2  14623  swrdfv2  14624  swrdlsw  14630  swrdccat2  14632  pfxid  14647  pfxn0  14649  pfxnd0  14651  addlenpfx  14653  pfxtrcfv0  14656  pfxeq  14658  pfxtrcfvl  14659  pfxsuffeqwrdeq  14660  pfxccat1  14664  pfxcctswrd  14672  ccats1pfxeq  14676  ccats1pfxeqrex  14677  ccatopth2  14679  cats1un  14683  wrdind  14684  wrd2ind  14685  swrdccatin1  14687  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccatin12lem3  14694  pfxccatin12  14695  pfxccat3  14696  swrdccat  14697  pfxccatpfx2  14699  pfxccat3a  14700  swrdccat3blem  14701  swrdccat3b  14702  pfxccatid  14703  ccats1pfxeqbi  14704  spllen  14716  splfv1  14717  splfv2a  14718  splval2  14719  revcl  14723  revlen  14724  revccat  14728  revrev  14729  repswsymball  14741  repswsymballbi  14742  cshw0  14756  cshwsublen  14758  cshwn  14759  cshwlen  14761  cshwidxmod  14765  2cshwid  14776  3cshw  14780  cshweqdif2  14781  cshw1  14784  scshwfzeqfzo  14788  revco  14796  ccatco  14797  cats1fvn  14820  cats1fv  14821  pfx2  14909  swrd2lsw  14914  2swrd2eqwrdeq  14915  ccat2s1fvwALT  14917  cshwshashnsame  17074  chnind  18587  chnub  18588  chnlt  18589  chnccats1  18591  chnccat  18592  chnrev  18593  chnpolleha  18598  chnpolfz  18599  gsmsymgrfixlem1  19402  gsmsymgreqlem2  19406  pmtrdifwrdellem2  19457  psgnuni  19474  psgnran  19490  efginvrel2  19702  efgsdmi  19707  efgsval2  19708  efgsp1  19712  efgsfo  19714  efgredlemf  19716  efgredlemg  19717  efgredleme  19718  efgredlemd  19719  efgredlemc  19720  efgredlem  19722  efgred  19723  efgcpbllemb  19730  frgpuplem  19747  frgpnabllem1  19848  pgpfaclem1  20058  psgnghm  21560  upgrewlkle2  29675  wlkcl  29684  wlkeq  29702  wlkv0  29718  wlklenvclwlk  29722  redwlklem  29738  wlkp1lem3  29742  wlkp1lem8  29747  wlkdlem1  29749  pthdlem1  29834  pthdlem2  29836  wlkiswwlks1  29935  wlkiswwlks2lem1  29937  wlkiswwlks2lem3  29939  wlkiswwlks2lem4  29940  wwlksm1edg  29949  wlklnwwlkln2lem  29950  wwlksnextbi  29962  wwlksnextproplem2  29978  wwlksnextproplem3  29979  rusgrnumwwlks  30045  clwwlkccatlem  30059  umgrclwwlkge2  30061  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a2  30063  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlklem3  30071  clwlkclwwlk  30072  clwlkclwwlk2  30073  clwlkclwwlkfo  30079  clwwisshclwwslem  30084  erclwwlkref  30090  clwwlkn  30096  clwwlkwwlksb  30124  clwlknf1oclwwlknlem1  30151  clwwlknonex2lem2  30178  eupth2eucrct  30287  eucrctshift  30313  numclwlk2lem2f1o  30449  ccatf1  33009  pfxlsw2ccat  33010  ccatws1f1o  33011  ccatws1f1olast  33012  wrdt2ind  33013  splfv3  33018  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  cycpmfv1  33174  cycpmfv2  33175  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  cycpmrn  33204  cyc3genpm  33213  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  dfufd2lem  33609  sseqfv1  34533  sseqfn  34534  sseqmw  34535  sseqf  34536  sseqfv2  34538  sseqp1  34539  ofcccat  34687  signstlen  34711  signstfvn  34713  signstfvp  34715  signstfvneq0  34716  signstfvc  34718  signstfveq0a  34720  signstfveq0  34721  signshf  34732  signshlen  34734  signshnz  34735  lpadlem3  34822  lpadlem2  34824  lpadlen2  34825  lpadmax  34826  lpadleft  34827  lpadright  34828  revpfxsfxrev  35298  revwlk  35307  elmrsubrn  35702  ccatcan2d  42690  chnsubseqword  47308  chnsubseqwl  47309  chnsubseq  47310  chnsuslle  47311  chnerlem1  47312  chnerlem2  47313  lswn0  47904