Theorem lencl 14507

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

Syntax hints:   → wi 4   ∈ wcel 2099  ‘cfv 6542  Fincfn 8955  ℕ₀cn0 12494  ♯chash 14313  Word cword 14488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-n0 12495  df-z 12581  df-uz 12845  df-fz 13509  df-fzo 13652  df-hash 14314  df-word 14489

This theorem is referenced by:  wrdffz  14509  wrdnfi  14522  wrdsymb0  14523  wrdlenge1n0  14524  wrdlenge2n0  14526  wrdsymb1  14527  eqwrd  14531  wrdred1  14534  wrdred1hash  14535  ccatcl  14548  ccatlen  14549  ccat0  14550  ccatval1  14551  ccatval3  14553  elfzelfzccat  14554  ccatsymb  14556  ccatfv0  14557  ccatval21sw  14559  ccatlid  14560  ccatrid  14561  ccatass  14562  ccatrn  14563  lswccatn0lsw  14565  ccatalpha  14567  ccatws1lenp1b  14595  wrdlenccats1lenm1  14596  ccatw2s1len  14599  ccats1val2  14601  ccatws1n0  14606  lswccats1fst  14609  ccatw2s1p1  14610  ccat2s1fvw  14612  swrdnd  14628  swrdnd2  14629  swrdnd0  14631  swrdrlen  14633  swrdlen2  14634  swrdfv2  14635  swrdlsw  14641  swrdccat2  14643  pfxid  14658  pfxn0  14660  pfxnd0  14662  addlenrevpfx  14664  addlenpfx  14665  pfxtrcfv0  14668  pfxeq  14670  pfxtrcfvl  14671  pfxsuffeqwrdeq  14672  pfxccat1  14676  pfxcctswrd  14684  ccats1pfxeq  14688  ccats1pfxeqrex  14689  ccatopth2  14691  cats1un  14695  wrdind  14696  wrd2ind  14697  swrdccatin1  14699  swrdccatin2  14703  pfxccatin12lem2  14705  pfxccatin12lem3  14706  pfxccatin12  14707  pfxccat3  14708  swrdccat  14709  pfxccatpfx2  14711  pfxccat3a  14712  swrdccat3blem  14713  swrdccat3b  14714  pfxccatid  14715  ccats1pfxeqbi  14716  spllen  14728  splfv1  14729  splfv2a  14730  splval2  14731  revcl  14735  revlen  14736  revccat  14740  revrev  14741  repswsymball  14753  repswsymballbi  14754  cshw0  14768  cshwsublen  14770  cshwn  14771  cshwlen  14773  cshwidxmod  14777  2cshwid  14788  3cshw  14792  cshweqdif2  14793  cshw1  14796  scshwfzeqfzo  14801  revco  14809  ccatco  14810  cats1fvn  14833  cats1fv  14834  pfx2  14922  swrd2lsw  14927  2swrd2eqwrdeq  14928  ccat2s1fvwALT  14930  cshwshashnsame  17064  gsmsymgrfixlem1  19373  gsmsymgreqlem2  19377  pmtrdifwrdellem2  19428  psgnuni  19445  psgnran  19461  efginvrel2  19673  efgsdmi  19678  efgsval2  19679  efgsp1  19683  efgsfo  19685  efgredlemf  19687  efgredlemg  19688  efgredleme  19689  efgredlemd  19690  efgredlemc  19691  efgredlem  19693  efgred  19694  efgcpbllemb  19701  frgpuplem  19718  frgpnabllem1  19819  pgpfaclem1  20029  psgnghm  21499  upgrewlkle2  29407  wlkcl  29416  wlkeq  29435  wlkv0  29452  wlklenvclwlk  29456  redwlklem  29472  wlkp1lem3  29476  wlkp1lem8  29481  wlkdlem1  29483  pthdlem1  29567  pthdlem2  29569  wlkiswwlks1  29665  wlkiswwlks2lem1  29667  wlkiswwlks2lem3  29669  wlkiswwlks2lem4  29670  wwlksm1edg  29679  wlklnwwlkln2lem  29680  wwlksnextbi  29692  wwlksnextproplem2  29708  wwlksnextproplem3  29709  rusgrnumwwlks  29772  clwwlkccatlem  29786  umgrclwwlkge2  29788  clwlkclwwlklem2a1  29789  clwlkclwwlklem2a2  29790  clwlkclwwlklem2a4  29794  clwlkclwwlklem2a  29795  clwlkclwwlklem2  29797  clwlkclwwlklem3  29798  clwlkclwwlk  29799  clwlkclwwlk2  29800  clwlkclwwlkfo  29806  clwwisshclwwslem  29811  erclwwlkref  29817  clwwlkn  29823  clwwlkwwlksb  29851  clwlknf1oclwwlknlem1  29878  clwwlknonex2lem2  29905  eupth2eucrct  30014  eucrctshift  30040  numclwlk2lem2f1o  30176  ccatf1  32654  pfxlsw2ccat  32655  wrdt2ind  32656  splfv3  32661  cycpmfv1  32812  cycpmfv2  32813  cycpmco2f1  32823  cycpmco2rn  32824  cycpmco2lem3  32827  cycpmco2lem4  32828  cycpmco2lem5  32829  cycpmco2lem6  32830  cycpmco2lem7  32831  cycpmco2  32832  cycpmrn  32842  cyc3genpm  32851  sseqfv1  33945  sseqfn  33946  sseqmw  33947  sseqf  33948  sseqfv2  33950  sseqp1  33951  ofcccat  34111  signstlen  34135  signstfvn  34137  signstfvp  34139  signstfvneq0  34140  signstfvc  34142  signstfveq0a  34144  signstfveq0  34145  signshf  34156  signshlen  34158  signshnz  34159  lpadlem3  34246  lpadlem2  34248  lpadlen2  34249  lpadmax  34250  lpadleft  34251  lpadright  34252  revpfxsfxrev  34661  revwlk  34670  elmrsubrn  35066  ccatcan2d  41655  lswn0  46707