Theorem lencl 14598

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6533  Fincfn 8952  ℕ₀cn0 12528  ♯chash 14394  Word cword 14578

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-card 9944  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-n0 12529  df-z 12616  df-uz 12888  df-fz 13562  df-fzo 13710  df-hash 14395  df-word 14579

This theorem is used by:  wrdffz  14600  wrdnfi  14613  wrdsymb0  14614  wrdlenge1n0  14615  wrdlenge2n0  14617  wrdsymb1  14618  eqwrd  14622  wrdred1  14625  wrdred1hash  14626  ccatcl  14639  ccatlen  14640  ccat0  14641  ccatval1  14642  ccatval3  14644  elfzelfzccat  14645  ccatdmss  14647  ccatsymb  14648  ccatfv0  14649  ccatval21sw  14651  ccatlid  14652  ccatrid  14653  ccatass  14654  ccatrn  14655  ccatf1  14656  lswccatn0lsw  14658  ccatalpha  14660  ccatws1lenp1b  14689  wrdlenccats1lenm1  14690  ccatw2s1len  14693  ccats1val2  14695  ccatws1n0  14700  lswccats1fst  14703  ccatw2s1p1  14704  ccat2s1fvw  14706  swrdnd  14724  swrdnd2  14725  swrdnd0  14727  swrdrlen  14729  swrdlen2  14730  swrdfv2  14731  swrdlsw  14737  swrdccat2  14739  pfxid  14754  pfxn0  14756  pfxnd0  14758  addlenpfx  14760  pfxtrcfv0  14763  pfxeq  14765  pfxtrcfvl  14766  pfxsuffeqwrdeq  14767  pfxccat1  14771  pfxcctswrd  14779  ccats1pfxeq  14783  ccats1pfxeqrex  14784  ccatopth2  14786  cats1un  14790  wrdind  14791  wrd2ind  14792  swrdccatin1  14794  swrdccatin2  14798  pfxccatin12lem2  14800  pfxccatin12lem3  14801  pfxccatin12  14802  pfxccat3  14803  swrdccat  14804  pfxccatpfx2  14806  pfxccat3a  14807  swrdccat3blem  14808  swrdccat3b  14809  pfxccatid  14810  ccats1pfxeqbi  14811  spllen  14823  splfv1  14824  splfv2a  14825  splval2  14826  revcl  14830  revlen  14831  revccat  14835  revrev  14836  revpfxsfxrev  14837  repswsymball  14850  repswsymballbi  14851  cshw0  14865  cshwsublen  14867  cshwn  14868  cshwlen  14870  cshwidxmod  14874  2cshwid  14885  3cshw  14889  cshweqdif2  14890  cshw1  14893  scshwfzeqfzo  14897  revco  14905  ccatco  14906  cats1fvn  14929  cats1fv  14930  pfx2  15018  swrd2lsw  15025  2swrd2eqwrdeq  15026  ccat2s1fvwALT  15028  cshwshashnsame  17195  chnind  18709  chnub  18710  chnlt  18711  chnccats1  18713  chnccat  18714  chnrev  18715  chnpolleha  18720  chnpolfz  18721  gsmsymgrfixlem1  19554  gsmsymgreqlem2  19558  pmtrdifwrdellem2  19609  psgnuni  19626  psgnran  19642  efginvrel2  19854  efgsdmi  19859  efgsval2  19860  efgsp1  19864  efgsfo  19866  efgredlemf  19868  efgredlemg  19869  efgredleme  19870  efgredlemd  19871  efgredlemc  19872  efgredlem  19874  efgred  19875  efgcpbllemb  19882  frgpuplem  19899  frgpnabllem1  20000  pgpfaclem1  20210  psgnghm  21793  upgrewlkle2  30066  wlkcl  30075  wlkeq  30093  wlkv0  30109  wlklenvclwlk  30113  redwlklem  30129  wlkp1lem3  30133  wlkp1lem8  30138  wlkdlem1  30140  revwlk  30146  pthdlem1  30231  pthdlem2  30233  wlkiswwlks1  30335  wlkiswwlks2lem1  30337  wlkiswwlks2lem3  30339  wlkiswwlks2lem4  30340  wwlksm1edg  30349  wlklnwwlkln2lem  30350  wwlksnextbi  30362  wwlksnextproplem2  30378  wwlksnextproplem3  30379  rusgrnumwwlks  30445  clwwlkccatlem  30459  umgrclwwlkge2  30461  clwlkclwwlklem2a1  30462  clwlkclwwlklem2a2  30463  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwlkclwwlklem2  30470  clwlkclwwlklem3  30471  clwlkclwwlk  30472  clwlkclwwlk2  30473  clwlkclwwlkfo  30479  clwwisshclwwslem  30484  erclwwlkref  30490  clwwlkn  30496  clwwlkwwlksb  30524  clwlknf1oclwwlknlem1  30551  clwwlknonex2lem2  30578  eupth2eucrct  30697  eucrctshift  30723  numclwlk2lem2f1o  30859  pfxlsw2ccat  33392  ccatws1f1o  33393  ccatws1f1olast  33394  wrdt2ind  33395  splfv3  33398  gsumwrd2dccatlem  33517  gsumwrd2dccat  33518  cycpmfv1  33553  cycpmfv2  33554  cycpmco2f1  33564  cycpmco2rn  33565  cycpmco2lem3  33568  cycpmco2lem4  33569  cycpmco2lem5  33570  cycpmco2lem6  33571  cycpmco2lem7  33572  cycpmco2  33573  cycpmrn  33583  cyc3genpm  33592  1arithidomlem1  33945  1arithidomlem2  33946  1arithidom  33947  dfufd2lem  33959  sseqfv1  34900  sseqfn  34901  sseqmw  34902  sseqf  34903  sseqfv2  34905  sseqp1  34906  ofcccat  35054  signstlen  35075  signstfvn  35077  signstfvp  35079  signstfvneq0  35080  signstfvc  35082  signstfveq0a  35084  signstfveq0  35085  signshf  35096  signshlen  35098  signshnz  35099  lpadlem3  35189  lpadlem2  35191  lpadlen2  35192  lpadmax  35193  lpadleft  35194  lpadright  35195  elmrsubrn  36099  ccatcan2d  43118  chnsubseqword  47706  chnsubseqwl  47707  chnsubseq  47708  chnsuslle  47709  chnerlem1  47710  chnerlem2  47711  lswn0  48344