Theorem lencl 14236

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6433  Fincfn 8733  ℕ₀cn0 12233  ♯chash 14044  Word cword 14217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240  df-fzo 13383  df-hash 14045  df-word 14218

This theorem is referenced by:  wrdffz  14238  wrdnfi  14251  wrdsymb0  14252  wrdlenge1n0  14253  wrdlenge2n0  14255  wrdsymb1  14256  eqwrd  14260  wrdred1  14263  wrdred1hash  14264  ccatcl  14277  ccatlen  14278  ccatlenOLD  14279  ccat0  14280  ccatval1  14281  ccatval1OLD  14282  ccatval3  14284  elfzelfzccat  14285  ccatsymb  14287  ccatfv0  14288  ccatval21sw  14290  ccatlid  14291  ccatrid  14292  ccatass  14293  ccatrn  14294  lswccatn0lsw  14296  ccatalpha  14298  ccatws1lenp1b  14326  wrdlenccats1lenm1  14327  ccatw2s1len  14331  ccats1val2  14334  ccatws1n0  14342  lswccats1fst  14345  ccatw2s1p1  14346  ccatw2s1p1OLD  14347  ccat2s1fvw  14349  ccat2s1fvwOLD  14350  swrdnd  14367  swrdnd2  14368  swrdnd0  14370  swrdrlen  14372  swrdlen2  14373  swrdfv2  14374  swrdlsw  14380  swrdccat2  14382  pfxid  14397  pfxn0  14399  pfxnd0  14401  addlenrevpfx  14403  addlenpfx  14404  pfxtrcfv0  14407  pfxeq  14409  pfxtrcfvl  14410  pfxsuffeqwrdeq  14411  pfxccat1  14415  pfxcctswrd  14423  ccats1pfxeq  14427  ccats1pfxeqrex  14428  ccatopth2  14430  cats1un  14434  wrdind  14435  wrd2ind  14436  swrdccatin1  14438  swrdccatin2  14442  pfxccatin12lem2  14444  pfxccatin12lem3  14445  pfxccatin12  14446  pfxccat3  14447  swrdccat  14448  pfxccatpfx2  14450  pfxccat3a  14451  swrdccat3blem  14452  swrdccat3b  14453  pfxccatid  14454  ccats1pfxeqbi  14455  spllen  14467  splfv1  14468  splfv2a  14469  splval2  14470  revcl  14474  revlen  14475  revccat  14479  revrev  14480  repswsymball  14492  repswsymballbi  14493  cshw0  14507  cshwsublen  14509  cshwn  14510  cshwlen  14512  cshwidxmod  14516  2cshwid  14527  3cshw  14531  cshweqdif2  14532  cshw1  14535  scshwfzeqfzo  14539  revco  14547  ccatco  14548  cats1fvn  14571  cats1fv  14572  pfx2  14660  swrd2lsw  14665  2swrd2eqwrdeq  14666  ccat2s1fvwALT  14669  ccat2s1fvwALTOLD  14670  cshwshashnsame  16805  gsmsymgrfixlem1  19035  gsmsymgreqlem2  19039  pmtrdifwrdellem2  19090  psgnuni  19107  psgnran  19123  efginvrel2  19333  efgsdmi  19338  efgsval2  19339  efgsp1  19343  efgsfo  19345  efgredlemf  19347  efgredlemg  19348  efgredleme  19349  efgredlemd  19350  efgredlemc  19351  efgredlem  19353  efgred  19354  efgcpbllemb  19361  frgpuplem  19378  frgpnabllem1  19474  pgpfaclem1  19684  psgnghm  20785  upgrewlkle2  27973  wlkcl  27982  wlkeq  28001  wlkv0  28018  wlklenvclwlk  28022  wlklenvclwlkOLD  28023  redwlklem  28039  wlkp1lem3  28043  wlkp1lem8  28048  wlkdlem1  28050  pthdlem1  28134  pthdlem2  28136  wlkiswwlks1  28232  wlkiswwlks2lem1  28234  wlkiswwlks2lem3  28236  wlkiswwlks2lem4  28237  wwlksm1edg  28246  wlklnwwlkln2lem  28247  wwlksnextbi  28259  wwlksnextproplem2  28275  wwlksnextproplem3  28276  rusgrnumwwlks  28339  clwwlkccatlem  28353  umgrclwwlkge2  28355  clwlkclwwlklem2a1  28356  clwlkclwwlklem2a2  28357  clwlkclwwlklem2a4  28361  clwlkclwwlklem2a  28362  clwlkclwwlklem2  28364  clwlkclwwlklem3  28365  clwlkclwwlk  28366  clwlkclwwlk2  28367  clwlkclwwlkfo  28373  clwwisshclwwslem  28378  erclwwlkref  28384  clwwlkn  28390  clwwlkwwlksb  28418  clwlknf1oclwwlknlem1  28445  clwwlknonex2lem2  28472  eupth2eucrct  28581  eucrctshift  28607  numclwlk2lem2f1o  28743  ccatf1  31223  pfxlsw2ccat  31224  wrdt2ind  31225  splfv3  31230  cycpmfv1  31380  cycpmfv2  31381  cycpmco2f1  31391  cycpmco2rn  31392  cycpmco2lem3  31395  cycpmco2lem4  31396  cycpmco2lem5  31397  cycpmco2lem6  31398  cycpmco2lem7  31399  cycpmco2  31400  cycpmrn  31410  cyc3genpm  31419  sseqfv1  32356  sseqfn  32357  sseqmw  32358  sseqf  32359  sseqfv2  32361  sseqp1  32362  ofcccat  32522  signstlen  32546  signstfvn  32548  signstfvp  32550  signstfvneq0  32551  signstfvc  32553  signstfveq0a  32555  signstfveq0  32556  signshf  32567  signshlen  32569  signshnz  32570  lpadlem3  32658  lpadlem2  32660  lpadlen2  32661  lpadmax  32662  lpadleft  32663  lpadright  32664  revpfxsfxrev  33077  revwlk  33086  elmrsubrn  33482  ccatcan2d  40219  lswn0  44896