Theorem lencl 14088

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

Syntax hints:   → wi 4   ∈ wcel 2110  ‘cfv 6380  Fincfn 8626  ℕ₀cn0 12090  ♯chash 13896  Word cword 14069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177  df-uz 12439  df-fz 13096  df-fzo 13239  df-hash 13897  df-word 14070

This theorem is referenced by:  wrdffz  14090  wrdnfi  14103  wrdsymb0  14104  wrdlenge1n0  14105  wrdlenge2n0  14107  wrdsymb1  14108  eqwrd  14112  wrdred1  14115  wrdred1hash  14116  ccatcl  14129  ccatlen  14130  ccatlenOLD  14131  ccat0  14132  ccatval1  14133  ccatval1OLD  14134  ccatval3  14136  elfzelfzccat  14137  ccatsymb  14139  ccatfv0  14140  ccatval21sw  14142  ccatlid  14143  ccatrid  14144  ccatass  14145  ccatrn  14146  lswccatn0lsw  14148  ccatalpha  14150  ccatws1lenp1b  14178  wrdlenccats1lenm1  14179  ccatw2s1len  14183  ccats1val2  14186  ccatws1n0  14194  lswccats1fst  14197  ccatw2s1p1  14198  ccatw2s1p1OLD  14199  ccat2s1fvw  14201  ccat2s1fvwOLD  14202  swrdnd  14219  swrdnd2  14220  swrdnd0  14222  swrdrlen  14224  swrdlen2  14225  swrdfv2  14226  swrdlsw  14232  swrdccat2  14234  pfxid  14249  pfxn0  14251  pfxnd0  14253  addlenrevpfx  14255  addlenpfx  14256  pfxtrcfv0  14259  pfxeq  14261  pfxtrcfvl  14262  pfxsuffeqwrdeq  14263  pfxccat1  14267  pfxcctswrd  14275  ccats1pfxeq  14279  ccats1pfxeqrex  14280  ccatopth2  14282  cats1un  14286  wrdind  14287  wrd2ind  14288  swrdccatin1  14290  swrdccatin2  14294  pfxccatin12lem2  14296  pfxccatin12lem3  14297  pfxccatin12  14298  pfxccat3  14299  swrdccat  14300  pfxccatpfx2  14302  pfxccat3a  14303  swrdccat3blem  14304  swrdccat3b  14305  pfxccatid  14306  ccats1pfxeqbi  14307  spllen  14319  splfv1  14320  splfv2a  14321  splval2  14322  revcl  14326  revlen  14327  revccat  14331  revrev  14332  repswsymball  14344  repswsymballbi  14345  cshw0  14359  cshwsublen  14361  cshwn  14362  cshwlen  14364  cshwidxmod  14368  2cshwid  14379  3cshw  14383  cshweqdif2  14384  cshw1  14387  scshwfzeqfzo  14391  revco  14399  ccatco  14400  cats1fvn  14423  cats1fv  14424  pfx2  14512  swrd2lsw  14517  2swrd2eqwrdeq  14518  ccat2s1fvwALT  14521  ccat2s1fvwALTOLD  14522  cshwshashnsame  16657  gsmsymgrfixlem1  18819  gsmsymgreqlem2  18823  pmtrdifwrdellem2  18874  psgnuni  18891  psgnran  18907  efginvrel2  19117  efgsdmi  19122  efgsval2  19123  efgsp1  19127  efgsfo  19129  efgredlemf  19131  efgredlemg  19132  efgredleme  19133  efgredlemd  19134  efgredlemc  19135  efgredlem  19137  efgred  19138  efgcpbllemb  19145  frgpuplem  19162  frgpnabllem1  19258  pgpfaclem1  19468  psgnghm  20542  upgrewlkle2  27694  wlkcl  27703  wlkeq  27721  wlkv0  27738  wlklenvclwlk  27742  wlklenvclwlkOLD  27743  redwlklem  27759  wlkp1lem3  27763  wlkp1lem8  27768  wlkdlem1  27770  pthdlem1  27853  pthdlem2  27855  wlkiswwlks1  27951  wlkiswwlks2lem1  27953  wlkiswwlks2lem3  27955  wlkiswwlks2lem4  27956  wwlksm1edg  27965  wlklnwwlkln2lem  27966  wwlksnextbi  27978  wwlksnextproplem2  27994  wwlksnextproplem3  27995  rusgrnumwwlks  28058  clwwlkccatlem  28072  umgrclwwlkge2  28074  clwlkclwwlklem2a1  28075  clwlkclwwlklem2a2  28076  clwlkclwwlklem2a4  28080  clwlkclwwlklem2a  28081  clwlkclwwlklem2  28083  clwlkclwwlklem3  28084  clwlkclwwlk  28085  clwlkclwwlk2  28086  clwlkclwwlkfo  28092  clwwisshclwwslem  28097  erclwwlkref  28103  clwwlkn  28109  clwwlkwwlksb  28137  clwlknf1oclwwlknlem1  28164  clwwlknonex2lem2  28191  eupth2eucrct  28300  eucrctshift  28326  numclwlk2lem2f1o  28462  ccatf1  30943  pfxlsw2ccat  30944  wrdt2ind  30945  splfv3  30950  cycpmfv1  31099  cycpmfv2  31100  cycpmco2f1  31110  cycpmco2rn  31111  cycpmco2lem3  31114  cycpmco2lem4  31115  cycpmco2lem5  31116  cycpmco2lem6  31117  cycpmco2lem7  31118  cycpmco2  31119  cycpmrn  31129  cyc3genpm  31138  sseqfv1  32068  sseqfn  32069  sseqmw  32070  sseqf  32071  sseqfv2  32073  sseqp1  32074  ofcccat  32234  signstlen  32258  signstfvn  32260  signstfvp  32262  signstfvneq0  32263  signstfvc  32265  signstfveq0a  32267  signstfveq0  32268  signshf  32279  signshlen  32281  signshnz  32282  lpadlem3  32370  lpadlem2  32372  lpadlen2  32373  lpadmax  32374  lpadleft  32375  lpadright  32376  revpfxsfxrev  32790  revwlk  32799  elmrsubrn  33195  ccatcan2d  39932  lswn0  44569