Theorem lencl 14454

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

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6490  Fincfn 8881  ℕ₀cn0 12399  ♯chash 14251  Word cword 14434

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  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 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-fin 8885  df-card 9849  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-n0 12400  df-z 12487  df-uz 12750  df-fz 13422  df-fzo 13569  df-hash 14252  df-word 14435

This theorem is referenced by:  wrdffz  14456  wrdnfi  14469  wrdsymb0  14470  wrdlenge1n0  14471  wrdlenge2n0  14473  wrdsymb1  14474  eqwrd  14478  wrdred1  14481  wrdred1hash  14482  ccatcl  14495  ccatlen  14496  ccat0  14497  ccatval1  14498  ccatval3  14500  elfzelfzccat  14501  ccatdmss  14503  ccatsymb  14504  ccatfv0  14505  ccatval21sw  14507  ccatlid  14508  ccatrid  14509  ccatass  14510  ccatrn  14511  lswccatn0lsw  14513  ccatalpha  14515  ccatws1lenp1b  14543  wrdlenccats1lenm1  14544  ccatw2s1len  14547  ccats1val2  14549  ccatws1n0  14554  lswccats1fst  14557  ccatw2s1p1  14558  ccat2s1fvw  14560  swrdnd  14576  swrdnd2  14577  swrdnd0  14579  swrdrlen  14581  swrdlen2  14582  swrdfv2  14583  swrdlsw  14589  swrdccat2  14591  pfxid  14606  pfxn0  14608  pfxnd0  14610  addlenpfx  14612  pfxtrcfv0  14615  pfxeq  14617  pfxtrcfvl  14618  pfxsuffeqwrdeq  14619  pfxccat1  14623  pfxcctswrd  14631  ccats1pfxeq  14635  ccats1pfxeqrex  14636  ccatopth2  14638  cats1un  14642  wrdind  14643  wrd2ind  14644  swrdccatin1  14646  swrdccatin2  14650  pfxccatin12lem2  14652  pfxccatin12lem3  14653  pfxccatin12  14654  pfxccat3  14655  swrdccat  14656  pfxccatpfx2  14658  pfxccat3a  14659  swrdccat3blem  14660  swrdccat3b  14661  pfxccatid  14662  ccats1pfxeqbi  14663  spllen  14675  splfv1  14676  splfv2a  14677  splval2  14678  revcl  14682  revlen  14683  revccat  14687  revrev  14688  repswsymball  14700  repswsymballbi  14701  cshw0  14715  cshwsublen  14717  cshwn  14718  cshwlen  14720  cshwidxmod  14724  2cshwid  14735  3cshw  14739  cshweqdif2  14740  cshw1  14743  scshwfzeqfzo  14747  revco  14755  ccatco  14756  cats1fvn  14779  cats1fv  14780  pfx2  14868  swrd2lsw  14873  2swrd2eqwrdeq  14874  ccat2s1fvwALT  14876  cshwshashnsame  17029  chnind  18542  chnub  18543  chnlt  18544  chnccats1  18546  chnccat  18547  chnrev  18548  chnpolleha  18553  chnpolfz  18554  gsmsymgrfixlem1  19354  gsmsymgreqlem2  19358  pmtrdifwrdellem2  19409  psgnuni  19426  psgnran  19442  efginvrel2  19654  efgsdmi  19659  efgsval2  19660  efgsp1  19664  efgsfo  19666  efgredlemf  19668  efgredlemg  19669  efgredleme  19670  efgredlemd  19671  efgredlemc  19672  efgredlem  19674  efgred  19675  efgcpbllemb  19682  frgpuplem  19699  frgpnabllem1  19800  pgpfaclem1  20010  psgnghm  21533  upgrewlkle2  29629  wlkcl  29638  wlkeq  29656  wlkv0  29672  wlklenvclwlk  29676  redwlklem  29692  wlkp1lem3  29696  wlkp1lem8  29701  wlkdlem1  29703  pthdlem1  29788  pthdlem2  29790  wlkiswwlks1  29889  wlkiswwlks2lem1  29891  wlkiswwlks2lem3  29893  wlkiswwlks2lem4  29894  wwlksm1edg  29903  wlklnwwlkln2lem  29904  wwlksnextbi  29916  wwlksnextproplem2  29932  wwlksnextproplem3  29933  rusgrnumwwlks  29999  clwwlkccatlem  30013  umgrclwwlkge2  30015  clwlkclwwlklem2a1  30016  clwlkclwwlklem2a2  30017  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  clwlkclwwlklem3  30025  clwlkclwwlk  30026  clwlkclwwlk2  30027  clwlkclwwlkfo  30033  clwwisshclwwslem  30038  erclwwlkref  30044  clwwlkn  30050  clwwlkwwlksb  30078  clwlknf1oclwwlknlem1  30105  clwwlknonex2lem2  30132  eupth2eucrct  30241  eucrctshift  30267  numclwlk2lem2f1o  30403  ccatf1  32980  pfxlsw2ccat  32981  ccatws1f1o  32982  ccatws1f1olast  32983  wrdt2ind  32984  splfv3  32989  gsumwrd2dccatlem  33108  gsumwrd2dccat  33109  cycpmfv1  33144  cycpmfv2  33145  cycpmco2f1  33155  cycpmco2rn  33156  cycpmco2lem3  33159  cycpmco2lem4  33160  cycpmco2lem5  33161  cycpmco2lem6  33162  cycpmco2lem7  33163  cycpmco2  33164  cycpmrn  33174  cyc3genpm  33183  1arithidomlem1  33565  1arithidomlem2  33566  1arithidom  33567  dfufd2lem  33579  sseqfv1  34495  sseqfn  34496  sseqmw  34497  sseqf  34498  sseqfv2  34500  sseqp1  34501  ofcccat  34649  signstlen  34673  signstfvn  34675  signstfvp  34677  signstfvneq0  34678  signstfvc  34680  signstfveq0a  34682  signstfveq0  34683  signshf  34694  signshlen  34696  signshnz  34697  lpadlem3  34784  lpadlem2  34786  lpadlen2  34787  lpadmax  34788  lpadleft  34789  lpadright  34790  revpfxsfxrev  35259  revwlk  35268  elmrsubrn  35663  ccatcan2d  42448  chnsubseqword  47064  chnsubseqwl  47065  chnsubseq  47066  chnsuslle  47067  chnerlem1  47068  chnerlem2  47069  lswn0  47632