Theorem lencl 14685

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6543  Fincfn 8980  ℕ₀cn0 12613  ♯chash 14481  Word cword 14665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  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 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-1st 8005  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-1o 8483  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-fin 8984  df-card 10027  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-nn 12343  df-n0 12614  df-z 12701  df-uz 12973  df-fz 13647  df-fzo 13796  df-hash 14482  df-word 14666

This theorem is used by:  wrdffz  14687  wrdnfi  14700  wrdsymb0  14701  wrdlenge1n0  14702  wrdlenge2n0  14704  wrdsymb1  14705  eqwrd  14709  wrdred1  14712  wrdred1hash  14713  ccatcl  14726  ccatlen  14727  ccat0  14728  ccatval1  14729  ccatval3  14731  elfzelfzccat  14732  ccatdmss  14734  ccatsymb  14735  ccatfv0  14736  ccatval21sw  14738  ccatlid  14739  ccatrid  14740  ccatass  14741  ccatrn  14742  ccatf1  14743  lswccatn0lsw  14745  ccatalpha  14747  ccatws1lenp1b  14777  wrdlenccats1lenm1  14778  ccatw2s1len  14781  ccats1val2  14783  ccatws1n0  14788  lswccats1fst  14791  ccatw2s1p1  14792  ccat2s1fvw  14794  swrdnd  14812  swrdnd2  14813  swrdnd0  14815  swrdrlen  14817  swrdlen2  14818  swrdfv2  14819  swrdlsw  14825  swrdccat2  14827  pfxid  14842  pfxn0  14844  pfxnd0  14846  addlenpfx  14848  pfxtrcfv0  14851  pfxeq  14853  pfxtrcfvl  14854  pfxsuffeqwrdeq  14855  pfxccat1  14859  pfxcctswrd  14867  ccats1pfxeq  14871  ccats1pfxeqrex  14872  ccatopth2  14874  cats1un  14878  wrdind  14879  wrd2ind  14880  swrdccatin1  14882  swrdccatin2  14886  pfxccatin12lem2  14888  pfxccatin12lem3  14889  pfxccatin12  14890  pfxccat3  14891  swrdccat  14892  pfxccatpfx2  14894  pfxccat3a  14895  swrdccat3blem  14896  swrdccat3b  14897  pfxccatid  14898  ccats1pfxeqbi  14899  spllen  14911  splfv1  14912  splfv2a  14913  splval2  14914  revcl  14918  revlen  14919  revccat  14923  revrev  14924  revpfxsfxrev  14925  repswsymball  14938  repswsymballbi  14939  cshw0  14953  cshwsublen  14955  cshwn  14956  cshwlen  14958  cshwidxmod  14962  2cshwid  14973  3cshw  14977  cshweqdif2  14978  cshw1  14981  scshwfzeqfzo  14985  revco  14993  ccatco  14994  cats1fvn  15017  cats1fv  15018  pfx2  15107  swrd2lsw  15114  2swrd2eqwrdeq  15115  ccat2s1fvwALT  15117  cshwshashnsame  17290  chnind  18804  chnub  18805  chnlt  18806  chnccats1  18808  chnccat  18809  chnrev  18810  chnpolleha  18815  chnpolfz  18816  gsmsymgrfixlem1  19650  gsmsymgreqlem2  19654  pmtrdifwrdellem2  19705  psgnuni  19722  psgnran  19738  efginvrel2  19950  efgsdmi  19955  efgsval2  19956  efgsp1  19960  efgsfo  19962  efgredlemf  19964  efgredlemg  19965  efgredleme  19966  efgredlemd  19967  efgredlemc  19968  efgredlem  19970  efgred  19971  efgcpbllemb  19978  frgpuplem  19995  frgpnabllem1  20096  pgpfaclem1  20306  psgnghm  21895  upgrewlkle2  30196  wlkcl  30205  wlkeq  30223  wlkv0  30239  wlklenvclwlk  30243  redwlklem  30259  wlkp1lem3  30263  wlkp1lem8  30268  wlkdlem1  30270  revwlk  30276  pthdlem1  30361  pthdlem2  30363  wlkiswwlks1  30465  wlkiswwlks2lem1  30467  wlkiswwlks2lem3  30469  wlkiswwlks2lem4  30470  wwlksm1edg  30479  wlklnwwlkln2lem  30480  wwlksnextbi  30492  wwlksnextproplem2  30508  wwlksnextproplem3  30509  rusgrnumwwlks  30575  clwwlkccatlem  30589  umgrclwwlkge2  30591  clwlkclwwlklem2a1  30592  clwlkclwwlklem2a2  30593  clwlkclwwlklem2a4  30597  clwlkclwwlklem2a  30598  clwlkclwwlklem2  30600  clwlkclwwlklem3  30601  clwlkclwwlk  30602  clwlkclwwlk2  30603  clwlkclwwlkfo  30609  clwwisshclwwslem  30614  erclwwlkref  30620  clwwlkn  30626  clwwlkwwlksb  30654  clwlknf1oclwwlknlem1  30681  clwwlknonex2lem2  30708  eupth2eucrct  30827  eucrctshift  30853  numclwlk2lem2f1o  30989  pfxlsw2ccat  33563  ccatws1f1o  33564  ccatws1f1olast  33565  wrdt2ind  33566  splfv3  33569  gsumwrd2dccatlem  33688  gsumwrd2dccat  33689  cycpmfv1  33724  cycpmfv2  33725  cycpmco2f1  33735  cycpmco2rn  33736  cycpmco2lem3  33739  cycpmco2lem4  33740  cycpmco2lem5  33741  cycpmco2lem6  33742  cycpmco2lem7  33743  cycpmco2  33744  cycpmrn  33754  cyc3genpm  33763  1arithidomlem1  34117  1arithidomlem2  34118  1arithidom  34119  dfufd2lem  34131  sseqfv1  35071  sseqfn  35072  sseqmw  35073  sseqf  35074  sseqfv2  35076  sseqp1  35077  ofcccat  35225  signstlen  35246  signstfvn  35248  signstfvp  35250  signstfvneq0  35251  signstfvc  35253  signstfveq0a  35255  signstfveq0  35256  signshf  35267  signshlen  35269  signshnz  35270  lpadlem3  35360  lpadlem2  35362  lpadlen2  35363  lpadmax  35364  lpadleft  35365  lpadright  35366  elmrsubrn  36375  ccatcan2d  43411  chnsubseqword  47996  chnsubseqwl  47997  chnsubseq  47998  chnsuslle  47999  chnerlem1  48000  chnerlem2  48001  lswn0  48634