Theorem lencl 14671

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  Fincfn 8966  ℕ₀cn0 12599  ♯chash 14467  Word cword 14651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-n0 12600  df-z 12687  df-uz 12959  df-fz 13633  df-fzo 13782  df-hash 14468  df-word 14652

This theorem is used by:  wrdffz  14673  wrdnfi  14686  wrdsymb0  14687  wrdlenge1n0  14688  wrdlenge2n0  14690  wrdsymb1  14691  eqwrd  14695  wrdred1  14698  wrdred1hash  14699  ccatcl  14712  ccatlen  14713  ccat0  14714  ccatval1  14715  ccatval3  14717  elfzelfzccat  14718  ccatdmss  14720  ccatsymb  14721  ccatfv0  14722  ccatval21sw  14724  ccatlid  14725  ccatrid  14726  ccatass  14727  ccatrn  14728  ccatf1  14729  lswccatn0lsw  14731  ccatalpha  14733  ccatws1lenp1b  14762  wrdlenccats1lenm1  14763  ccatw2s1len  14766  ccats1val2  14768  ccatws1n0  14773  lswccats1fst  14776  ccatw2s1p1  14777  ccat2s1fvw  14779  swrdnd  14797  swrdnd2  14798  swrdnd0  14800  swrdrlen  14802  swrdlen2  14803  swrdfv2  14804  swrdlsw  14810  swrdccat2  14812  pfxid  14827  pfxn0  14829  pfxnd0  14831  addlenpfx  14833  pfxtrcfv0  14836  pfxeq  14838  pfxtrcfvl  14839  pfxsuffeqwrdeq  14840  pfxccat1  14844  pfxcctswrd  14852  ccats1pfxeq  14856  ccats1pfxeqrex  14857  ccatopth2  14859  cats1un  14863  wrdind  14864  wrd2ind  14865  swrdccatin1  14867  swrdccatin2  14871  pfxccatin12lem2  14873  pfxccatin12lem3  14874  pfxccatin12  14875  pfxccat3  14876  swrdccat  14877  pfxccatpfx2  14879  pfxccat3a  14880  swrdccat3blem  14881  swrdccat3b  14882  pfxccatid  14883  ccats1pfxeqbi  14884  spllen  14896  splfv1  14897  splfv2a  14898  splval2  14899  revcl  14903  revlen  14904  revccat  14908  revrev  14909  revpfxsfxrev  14910  repswsymball  14923  repswsymballbi  14924  cshw0  14938  cshwsublen  14940  cshwn  14941  cshwlen  14943  cshwidxmod  14947  2cshwid  14958  3cshw  14962  cshweqdif2  14963  cshw1  14966  scshwfzeqfzo  14970  revco  14978  ccatco  14979  cats1fvn  15002  cats1fv  15003  pfx2  15091  swrd2lsw  15098  2swrd2eqwrdeq  15099  ccat2s1fvwALT  15101  cshwshashnsame  17274  chnind  18788  chnub  18789  chnlt  18790  chnccats1  18792  chnccat  18793  chnrev  18794  chnpolleha  18799  chnpolfz  18800  gsmsymgrfixlem1  19634  gsmsymgreqlem2  19638  pmtrdifwrdellem2  19689  psgnuni  19706  psgnran  19722  efginvrel2  19934  efgsdmi  19939  efgsval2  19940  efgsp1  19944  efgsfo  19946  efgredlemf  19948  efgredlemg  19949  efgredleme  19950  efgredlemd  19951  efgredlemc  19952  efgredlem  19954  efgred  19955  efgcpbllemb  19962  frgpuplem  19979  frgpnabllem1  20080  pgpfaclem1  20290  psgnghm  21879  upgrewlkle2  30180  wlkcl  30189  wlkeq  30207  wlkv0  30223  wlklenvclwlk  30227  redwlklem  30243  wlkp1lem3  30247  wlkp1lem8  30252  wlkdlem1  30254  revwlk  30260  pthdlem1  30345  pthdlem2  30347  wlkiswwlks1  30449  wlkiswwlks2lem1  30451  wlkiswwlks2lem3  30453  wlkiswwlks2lem4  30454  wwlksm1edg  30463  wlklnwwlkln2lem  30464  wwlksnextbi  30476  wwlksnextproplem2  30492  wwlksnextproplem3  30493  rusgrnumwwlks  30559  clwwlkccatlem  30573  umgrclwwlkge2  30575  clwlkclwwlklem2a1  30576  clwlkclwwlklem2a2  30577  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwlkclwwlklem2  30584  clwlkclwwlklem3  30585  clwlkclwwlk  30586  clwlkclwwlk2  30587  clwlkclwwlkfo  30593  clwwisshclwwslem  30598  erclwwlkref  30604  clwwlkn  30610  clwwlkwwlksb  30638  clwlknf1oclwwlknlem1  30665  clwwlknonex2lem2  30692  eupth2eucrct  30811  eucrctshift  30837  numclwlk2lem2f1o  30973  pfxlsw2ccat  33506  ccatws1f1o  33507  ccatws1f1olast  33508  wrdt2ind  33509  splfv3  33512  gsumwrd2dccatlem  33631  gsumwrd2dccat  33632  cycpmfv1  33667  cycpmfv2  33668  cycpmco2f1  33678  cycpmco2rn  33679  cycpmco2lem3  33682  cycpmco2lem4  33683  cycpmco2lem5  33684  cycpmco2lem6  33685  cycpmco2lem7  33686  cycpmco2  33687  cycpmrn  33697  cyc3genpm  33706  1arithidomlem1  34060  1arithidomlem2  34061  1arithidom  34062  dfufd2lem  34074  sseqfv1  35014  sseqfn  35015  sseqmw  35016  sseqf  35017  sseqfv2  35019  sseqp1  35020  ofcccat  35168  signstlen  35189  signstfvn  35191  signstfvp  35193  signstfvneq0  35194  signstfvc  35196  signstfveq0a  35198  signstfveq0  35199  signshf  35210  signshlen  35212  signshnz  35213  lpadlem3  35303  lpadlem2  35305  lpadlen2  35306  lpadmax  35307  lpadleft  35308  lpadright  35309  elmrsubrn  36264  ccatcan2d  43282  chnsubseqword  47857  chnsubseqwl  47858  chnsubseq  47859  chnsuslle  47860  chnerlem1  47861  chnerlem2  47862  lswn0  48495