Theorem lencl 14474

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  Fincfn 8895  ℕ₀cn0 12418  ♯chash 14271  Word cword 14454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  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 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-n0 12419  df-z 12506  df-uz 12770  df-fz 13445  df-fzo 13592  df-hash 14272  df-word 14455

This theorem is referenced by:  wrdffz  14476  wrdnfi  14489  wrdsymb0  14490  wrdlenge1n0  14491  wrdlenge2n0  14493  wrdsymb1  14494  eqwrd  14498  wrdred1  14501  wrdred1hash  14502  ccatcl  14515  ccatlen  14516  ccat0  14517  ccatval1  14518  ccatval3  14520  elfzelfzccat  14521  ccatsymb  14523  ccatfv0  14524  ccatval21sw  14526  ccatlid  14527  ccatrid  14528  ccatass  14529  ccatrn  14530  lswccatn0lsw  14532  ccatalpha  14534  ccatws1lenp1b  14562  wrdlenccats1lenm1  14563  ccatw2s1len  14566  ccats1val2  14568  ccatws1n0  14573  lswccats1fst  14576  ccatw2s1p1  14577  ccat2s1fvw  14579  swrdnd  14595  swrdnd2  14596  swrdnd0  14598  swrdrlen  14600  swrdlen2  14601  swrdfv2  14602  swrdlsw  14608  swrdccat2  14610  pfxid  14625  pfxn0  14627  pfxnd0  14629  addlenrevpfx  14631  addlenpfx  14632  pfxtrcfv0  14635  pfxeq  14637  pfxtrcfvl  14638  pfxsuffeqwrdeq  14639  pfxccat1  14643  pfxcctswrd  14651  ccats1pfxeq  14655  ccats1pfxeqrex  14656  ccatopth2  14658  cats1un  14662  wrdind  14663  wrd2ind  14664  swrdccatin1  14666  swrdccatin2  14670  pfxccatin12lem2  14672  pfxccatin12lem3  14673  pfxccatin12  14674  pfxccat3  14675  swrdccat  14676  pfxccatpfx2  14678  pfxccat3a  14679  swrdccat3blem  14680  swrdccat3b  14681  pfxccatid  14682  ccats1pfxeqbi  14683  spllen  14695  splfv1  14696  splfv2a  14697  splval2  14698  revcl  14702  revlen  14703  revccat  14707  revrev  14708  repswsymball  14720  repswsymballbi  14721  cshw0  14735  cshwsublen  14737  cshwn  14738  cshwlen  14740  cshwidxmod  14744  2cshwid  14755  3cshw  14759  cshweqdif2  14760  cshw1  14763  scshwfzeqfzo  14768  revco  14776  ccatco  14777  cats1fvn  14800  cats1fv  14801  pfx2  14889  swrd2lsw  14894  2swrd2eqwrdeq  14895  ccat2s1fvwALT  14897  cshwshashnsame  17050  gsmsymgrfixlem1  19333  gsmsymgreqlem2  19337  pmtrdifwrdellem2  19388  psgnuni  19405  psgnran  19421  efginvrel2  19633  efgsdmi  19638  efgsval2  19639  efgsp1  19643  efgsfo  19645  efgredlemf  19647  efgredlemg  19648  efgredleme  19649  efgredlemd  19650  efgredlemc  19651  efgredlem  19653  efgred  19654  efgcpbllemb  19661  frgpuplem  19678  frgpnabllem1  19779  pgpfaclem1  19989  psgnghm  21465  upgrewlkle2  29510  wlkcl  29519  wlkeq  29537  wlkv0  29553  wlklenvclwlk  29557  redwlklem  29573  wlkp1lem3  29577  wlkp1lem8  29582  wlkdlem1  29584  pthdlem1  29669  pthdlem2  29671  wlkiswwlks1  29770  wlkiswwlks2lem1  29772  wlkiswwlks2lem3  29774  wlkiswwlks2lem4  29775  wwlksm1edg  29784  wlklnwwlkln2lem  29785  wwlksnextbi  29797  wwlksnextproplem2  29813  wwlksnextproplem3  29814  rusgrnumwwlks  29877  clwwlkccatlem  29891  umgrclwwlkge2  29893  clwlkclwwlklem2a1  29894  clwlkclwwlklem2a2  29895  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwlkclwwlklem2  29902  clwlkclwwlklem3  29903  clwlkclwwlk  29904  clwlkclwwlk2  29905  clwlkclwwlkfo  29911  clwwisshclwwslem  29916  erclwwlkref  29922  clwwlkn  29928  clwwlkwwlksb  29956  clwlknf1oclwwlknlem1  29983  clwwlknonex2lem2  30010  eupth2eucrct  30119  eucrctshift  30145  numclwlk2lem2f1o  30281  ccatf1  32843  ccatdmss  32844  pfxlsw2ccat  32845  ccatws1f1o  32846  ccatws1f1olast  32847  wrdt2ind  32848  splfv3  32853  chnind  32910  chnub  32911  chnlt  32912  chnccats1  32914  gsumwrd2dccatlem  32979  gsumwrd2dccat  32980  cycpmfv1  33043  cycpmfv2  33044  cycpmco2f1  33054  cycpmco2rn  33055  cycpmco2lem3  33058  cycpmco2lem4  33059  cycpmco2lem5  33060  cycpmco2lem6  33061  cycpmco2lem7  33062  cycpmco2  33063  cycpmrn  33073  cyc3genpm  33082  1arithidomlem1  33479  1arithidomlem2  33480  1arithidom  33481  dfufd2lem  33493  sseqfv1  34353  sseqfn  34354  sseqmw  34355  sseqf  34356  sseqfv2  34358  sseqp1  34359  ofcccat  34507  signstlen  34531  signstfvn  34533  signstfvp  34535  signstfvneq0  34536  signstfvc  34538  signstfveq0a  34540  signstfveq0  34541  signshf  34552  signshlen  34554  signshnz  34555  lpadlem3  34642  lpadlem2  34644  lpadlen2  34645  lpadmax  34646  lpadleft  34647  lpadright  34648  revpfxsfxrev  35076  revwlk  35085  elmrsubrn  35480  ccatcan2d  42212  lswn0  47418