Theorem lencl 14468

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6500  Fincfn 8895  ℕ₀cn0 12413  ♯chash 14265  Word cword 14448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-n0 12414  df-z 12501  df-uz 12764  df-fz 13436  df-fzo 13583  df-hash 14266  df-word 14449

This theorem is referenced by:  wrdffz  14470  wrdnfi  14483  wrdsymb0  14484  wrdlenge1n0  14485  wrdlenge2n0  14487  wrdsymb1  14488  eqwrd  14492  wrdred1  14495  wrdred1hash  14496  ccatcl  14509  ccatlen  14510  ccat0  14511  ccatval1  14512  ccatval3  14514  elfzelfzccat  14515  ccatdmss  14517  ccatsymb  14518  ccatfv0  14519  ccatval21sw  14521  ccatlid  14522  ccatrid  14523  ccatass  14524  ccatrn  14525  lswccatn0lsw  14527  ccatalpha  14529  ccatws1lenp1b  14557  wrdlenccats1lenm1  14558  ccatw2s1len  14561  ccats1val2  14563  ccatws1n0  14568  lswccats1fst  14571  ccatw2s1p1  14572  ccat2s1fvw  14574  swrdnd  14590  swrdnd2  14591  swrdnd0  14593  swrdrlen  14595  swrdlen2  14596  swrdfv2  14597  swrdlsw  14603  swrdccat2  14605  pfxid  14620  pfxn0  14622  pfxnd0  14624  addlenpfx  14626  pfxtrcfv0  14629  pfxeq  14631  pfxtrcfvl  14632  pfxsuffeqwrdeq  14633  pfxccat1  14637  pfxcctswrd  14645  ccats1pfxeq  14649  ccats1pfxeqrex  14650  ccatopth2  14652  cats1un  14656  wrdind  14657  wrd2ind  14658  swrdccatin1  14660  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12lem3  14667  pfxccatin12  14668  pfxccat3  14669  swrdccat  14670  pfxccatpfx2  14672  pfxccat3a  14673  swrdccat3blem  14674  swrdccat3b  14675  pfxccatid  14676  ccats1pfxeqbi  14677  spllen  14689  splfv1  14690  splfv2a  14691  splval2  14692  revcl  14696  revlen  14697  revccat  14701  revrev  14702  repswsymball  14714  repswsymballbi  14715  cshw0  14729  cshwsublen  14731  cshwn  14732  cshwlen  14734  cshwidxmod  14738  2cshwid  14749  3cshw  14753  cshweqdif2  14754  cshw1  14757  scshwfzeqfzo  14761  revco  14769  ccatco  14770  cats1fvn  14793  cats1fv  14794  pfx2  14882  swrd2lsw  14887  2swrd2eqwrdeq  14888  ccat2s1fvwALT  14890  cshwshashnsame  17043  chnind  18556  chnub  18557  chnlt  18558  chnccats1  18560  chnccat  18561  chnrev  18562  chnpolleha  18567  chnpolfz  18568  gsmsymgrfixlem1  19368  gsmsymgreqlem2  19372  pmtrdifwrdellem2  19423  psgnuni  19440  psgnran  19456  efginvrel2  19668  efgsdmi  19673  efgsval2  19674  efgsp1  19678  efgsfo  19680  efgredlemf  19682  efgredlemg  19683  efgredleme  19684  efgredlemd  19685  efgredlemc  19686  efgredlem  19688  efgred  19689  efgcpbllemb  19696  frgpuplem  19713  frgpnabllem1  19814  pgpfaclem1  20024  psgnghm  21547  upgrewlkle2  29692  wlkcl  29701  wlkeq  29719  wlkv0  29735  wlklenvclwlk  29739  redwlklem  29755  wlkp1lem3  29759  wlkp1lem8  29764  wlkdlem1  29766  pthdlem1  29851  pthdlem2  29853  wlkiswwlks1  29952  wlkiswwlks2lem1  29954  wlkiswwlks2lem3  29956  wlkiswwlks2lem4  29957  wwlksm1edg  29966  wlklnwwlkln2lem  29967  wwlksnextbi  29979  wwlksnextproplem2  29995  wwlksnextproplem3  29996  rusgrnumwwlks  30062  clwwlkccatlem  30076  umgrclwwlkge2  30078  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a2  30080  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlklem3  30088  clwlkclwwlk  30089  clwlkclwwlk2  30090  clwlkclwwlkfo  30096  clwwisshclwwslem  30101  erclwwlkref  30107  clwwlkn  30113  clwwlkwwlksb  30141  clwlknf1oclwwlknlem1  30168  clwwlknonex2lem2  30195  eupth2eucrct  30304  eucrctshift  30330  numclwlk2lem2f1o  30466  ccatf1  33042  pfxlsw2ccat  33043  ccatws1f1o  33044  ccatws1f1olast  33045  wrdt2ind  33046  splfv3  33051  gsumwrd2dccatlem  33171  gsumwrd2dccat  33172  cycpmfv1  33207  cycpmfv2  33208  cycpmco2f1  33218  cycpmco2rn  33219  cycpmco2lem3  33222  cycpmco2lem4  33223  cycpmco2lem5  33224  cycpmco2lem6  33225  cycpmco2lem7  33226  cycpmco2  33227  cycpmrn  33237  cyc3genpm  33246  1arithidomlem1  33628  1arithidomlem2  33629  1arithidom  33630  dfufd2lem  33642  sseqfv1  34567  sseqfn  34568  sseqmw  34569  sseqf  34570  sseqfv2  34572  sseqp1  34573  ofcccat  34721  signstlen  34745  signstfvn  34747  signstfvp  34749  signstfvneq0  34750  signstfvc  34752  signstfveq0a  34754  signstfveq0  34755  signshf  34766  signshlen  34768  signshnz  34769  lpadlem3  34856  lpadlem2  34858  lpadlen2  34859  lpadmax  34860  lpadleft  34861  lpadright  34862  revpfxsfxrev  35332  revwlk  35341  elmrsubrn  35736  ccatcan2d  42621  chnsubseqword  47236  chnsubseqwl  47237  chnsubseq  47238  chnsuslle  47239  chnerlem1  47240  chnerlem2  47241  lswn0  47804