Theorem lencl 14546

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

Syntax hints:   → wi 4   ∈ wcel 2142  ‘cfv 6521  Fincfn 8927  ℕ₀cn0 12481  ♯chash 14343  Word cword 14526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-card 9897  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-n0 12482  df-z 12569  df-uz 12840  df-fz 13513  df-fzo 13660  df-hash 14344  df-word 14527

This theorem is referenced by:  wrdffz  14548  wrdnfi  14561  wrdsymb0  14562  wrdlenge1n0  14563  wrdlenge2n0  14565  wrdsymb1  14566  eqwrd  14570  wrdred1  14573  wrdred1hash  14574  ccatcl  14587  ccatlen  14588  ccat0  14589  ccatval1  14590  ccatval3  14592  elfzelfzccat  14593  ccatdmss  14595  ccatsymb  14596  ccatfv0  14597  ccatval21sw  14599  ccatlid  14600  ccatrid  14601  ccatass  14602  ccatrn  14603  lswccatn0lsw  14605  ccatalpha  14607  ccatws1lenp1b  14635  wrdlenccats1lenm1  14636  ccatw2s1len  14639  ccats1val2  14641  ccatws1n0  14646  lswccats1fst  14649  ccatw2s1p1  14650  ccat2s1fvw  14652  swrdnd  14668  swrdnd2  14669  swrdnd0  14671  swrdrlen  14673  swrdlen2  14674  swrdfv2  14675  swrdlsw  14681  swrdccat2  14683  pfxid  14698  pfxn0  14700  pfxnd0  14702  addlenpfx  14704  pfxtrcfv0  14707  pfxeq  14709  pfxtrcfvl  14710  pfxsuffeqwrdeq  14711  pfxccat1  14715  pfxcctswrd  14723  ccats1pfxeq  14727  ccats1pfxeqrex  14728  ccatopth2  14730  cats1un  14734  wrdind  14735  wrd2ind  14736  swrdccatin1  14738  swrdccatin2  14742  pfxccatin12lem2  14744  pfxccatin12lem3  14745  pfxccatin12  14746  pfxccat3  14747  swrdccat  14748  pfxccatpfx2  14750  pfxccat3a  14751  swrdccat3blem  14752  swrdccat3b  14753  pfxccatid  14754  ccats1pfxeqbi  14755  spllen  14767  splfv1  14768  splfv2a  14769  splval2  14770  revcl  14774  revlen  14775  revccat  14779  revrev  14780  repswsymball  14792  repswsymballbi  14793  cshw0  14807  cshwsublen  14809  cshwn  14810  cshwlen  14812  cshwidxmod  14816  2cshwid  14827  3cshw  14831  cshweqdif2  14832  cshw1  14835  scshwfzeqfzo  14839  revco  14847  ccatco  14848  cats1fvn  14871  cats1fv  14872  pfx2  14960  swrd2lsw  14965  2swrd2eqwrdeq  14966  ccat2s1fvwALT  14968  cshwshashnsame  17139  chnind  18653  chnub  18654  chnlt  18655  chnccats1  18657  chnccat  18658  chnrev  18659  chnpolleha  18664  chnpolfz  18665  gsmsymgrfixlem1  19467  gsmsymgreqlem2  19471  pmtrdifwrdellem2  19522  psgnuni  19539  psgnran  19555  efginvrel2  19767  efgsdmi  19772  efgsval2  19773  efgsp1  19777  efgsfo  19779  efgredlemf  19781  efgredlemg  19782  efgredleme  19783  efgredlemd  19784  efgredlemc  19785  efgredlem  19787  efgred  19788  efgcpbllemb  19795  frgpuplem  19812  frgpnabllem1  19913  pgpfaclem1  20123  psgnghm  21629  upgrewlkle2  29804  wlkcl  29813  wlkeq  29831  wlkv0  29847  wlklenvclwlk  29851  redwlklem  29867  wlkp1lem3  29871  wlkp1lem8  29876  wlkdlem1  29878  pthdlem1  29963  pthdlem2  29965  wlkiswwlks1  30064  wlkiswwlks2lem1  30066  wlkiswwlks2lem3  30068  wlkiswwlks2lem4  30069  wwlksm1edg  30078  wlklnwwlkln2lem  30079  wwlksnextbi  30091  wwlksnextproplem2  30107  wwlksnextproplem3  30108  rusgrnumwwlks  30174  clwwlkccatlem  30188  umgrclwwlkge2  30190  clwlkclwwlklem2a1  30191  clwlkclwwlklem2a2  30192  clwlkclwwlklem2a4  30196  clwlkclwwlklem2a  30197  clwlkclwwlklem2  30199  clwlkclwwlklem3  30200  clwlkclwwlk  30201  clwlkclwwlk2  30202  clwlkclwwlkfo  30208  clwwisshclwwslem  30213  erclwwlkref  30219  clwwlkn  30225  clwwlkwwlksb  30253  clwlknf1oclwwlknlem1  30280  clwwlknonex2lem2  30307  eupth2eucrct  30416  eucrctshift  30442  numclwlk2lem2f1o  30578  ccatf1  33124  pfxlsw2ccat  33125  ccatws1f1o  33126  ccatws1f1olast  33127  wrdt2ind  33128  splfv3  33133  gsumwrd2dccatlem  33254  gsumwrd2dccat  33255  cycpmfv1  33290  cycpmfv2  33291  cycpmco2f1  33301  cycpmco2rn  33302  cycpmco2lem3  33305  cycpmco2lem4  33306  cycpmco2lem5  33307  cycpmco2lem6  33308  cycpmco2lem7  33309  cycpmco2  33310  cycpmrn  33320  cyc3genpm  33329  1arithidomlem1  33728  1arithidomlem2  33729  1arithidom  33730  dfufd2lem  33742  sseqfv1  34683  sseqfn  34684  sseqmw  34685  sseqf  34686  sseqfv2  34688  sseqp1  34689  ofcccat  34837  signstlen  34858  signstfvn  34860  signstfvp  34862  signstfvneq0  34863  signstfvc  34865  signstfveq0a  34867  signstfveq0  34868  signshf  34879  signshlen  34881  signshnz  34882  lpadlem3  34972  lpadlem2  34974  lpadlen2  34975  lpadmax  34976  lpadleft  34977  lpadright  34978  revpfxsfxrev  35463  revwlk  35472  elmrsubrn  35867  ccatcan2d  42864  chnsubseqword  47451  chnsubseqwl  47452  chnsubseq  47453  chnsuslle  47454  chnerlem1  47455  chnerlem2  47456  lswn0  48047