MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lencl Structured version   Visualization version   GIF version

Theorem lencl 13535
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
StepHypRef Expression
1 wrdfin 13534 . 2 (𝑊 ∈ Word 𝑆𝑊 ∈ Fin)
2 hashcl 13365 . 2 (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ0)
31, 2syl 17 1 (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  cfv 6101  Fincfn 8192  0cn0 11559  chash 13337  Word cword 13502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-oadd 7800  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-card 9048  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-n0 11560  df-z 11644  df-uz 11905  df-fz 12550  df-fzo 12690  df-hash 13338  df-word 13510
This theorem is referenced by:  wrdffz  13537  wrdsymb0  13550  wrdlenge1n0  13551  wrdlenge2n0  13553  wrdsymb1  13554  eqwrd  13558  wrdred1  13561  wrdred1hash  13562  ccatcl  13571  ccatlen  13572  ccat0  13573  ccatval1  13574  ccatval3  13576  elfzelfzccat  13577  ccatsymb  13579  ccatfv0  13580  ccatval21sw  13582  ccatlid  13583  ccatrid  13584  ccatass  13585  ccatrn  13586  lswccatn0lsw  13588  ccatalpha  13590  ccatws1lenp1b  13617  wrdlenccats1lenm1  13618  wrdlenccats1lenm1OLD  13619  ccatw2s1len  13622  ccatw2s1lenOLD  13623  ccats1val2  13625  ccat1st1st  13626  ccatws1lenrevOLD  13630  ccatws1n0  13631  ccatws1n0OLD  13632  lswccats1fst  13635  ccatw2s1p1  13636  ccat2s1fvw  13638  swrdid  13652  swrdn0  13654  swrdnd  13656  swrdnd2  13657  swrdrlen  13659  addlenrevswrd  13661  addlenswrd  13662  swrdtrcfv0  13666  swrdeq  13668  swrdlen2  13669  swrdfv2  13670  swrdtrcfvl  13674  swrdlsw  13676  2swrdeqwrdeq  13677  2swrd1eqwrdeq  13678  swrdccat1  13681  swrdccat2  13682  wrdcctswrd  13689  ccats1swrdeq  13693  ccatopth2  13695  cats1un  13699  wrdind  13700  wrd2ind  13701  ccats1swrdeqrex  13702  swrdccatin1  13707  swrdccatin2  13711  swrdccatin12lem2  13713  swrdccatin12lem3  13714  swrdccatin12  13715  swrdccat3  13716  swrdccat  13717  swrdccat3a  13718  swrdccat3blem  13719  swrdccat3b  13720  swrdccatid  13721  ccats1swrdeqbi  13722  spllen  13729  splval2  13732  revcl  13734  revlen  13735  revccat  13739  revrev  13740  repswsymball  13750  repswsymballbi  13751  cshwsublen  13766  cshwn  13767  cshwlen  13769  cshwidxmod  13773  2cshwid  13784  3cshw  13788  cshweqdif2  13789  cshw1  13792  scshwfzeqfzo  13796  revco  13804  ccatco  13805  cats1fvn  13827  cats1fv  13828  swrd2lsw  13920  2swrd2eqwrdeq  13921  ccat2s1fvwALT  13923  cshwshashnsame  16022  gsmsymgrfixlem1  18048  gsmsymgreqlem2  18052  pmtrdifwrdellem2  18103  psgnuni  18120  psgnran  18136  efginvrel2  18341  efgsdmi  18346  efgsval2  18347  efgsp1  18351  efgsfo  18353  efgredlemf  18355  efgredlemg  18356  efgredleme  18357  efgredlemd  18358  efgredlemc  18359  efgredlem  18361  efgred  18362  efgcpbllemb  18369  frgpuplem  18386  frgpnabllem1  18477  pgpfaclem1  18682  psgnghm  20133  upgrewlkle2  26730  wlkcl  26739  wlkeq  26757  wlkv0  26775  wlklenvclwlk  26779  redwlklem  26796  wlkp1lem3  26800  wlkp1lem8  26805  wlkdlem1  26807  pthdlem1  26890  pthdlem2  26892  wlkiswwlks1  26994  wlkiswwlks2lem1  26996  wlkiswwlks2lem3  26998  wlkiswwlks2lem4  26999  wwlksm1edg  27008  wlklnwwlkln2lem  27009  wwlksnextbi  27031  wwlksnextproplem2  27048  wwlksnextproplem3  27049  rusgrnumwwlks  27116  clwwlkccatlem  27132  umgrclwwlkge2  27134  clwlkclwwlklem2a1  27135  clwlkclwwlklem2a2  27136  clwlkclwwlklem2a4  27140  clwlkclwwlklem2a  27141  clwlkclwwlklem2  27143  clwlkclwwlklem3  27144  clwlkclwwlk  27145  clwlkclwwlk2  27146  clwlkclwwlkfo  27152  clwwisshclwwslem  27157  erclwwlkref  27163  clwwlkn  27171  clwwlkwwlksb  27204  clwlksfclwwlk2wrdOLD  27232  clwlksfclwwlk1hashOLD  27234  clwlksfclwwlkOLD  27236  clwlksf1clwwlklem1OLD  27239  clwlksf1clwwlklem3OLD  27241  clwlknf1oclwwlknlem1  27245  clwwlknonex2lem2  27277  eupth2eucrct  27390  eucrctshift  27416  numclwlk2lem2f1o  27559  numclwlk2lem2f1oOLD  27566  sseqfv1  30776  sseqfn  30777  sseqmw  30778  sseqf  30779  sseqfv2  30781  sseqp1  30782  signstlen  30969  signstfvn  30971  signstfvp  30973  signstfvneq0  30974  signstfvc  30976  signstfveq0a  30978  signstfveq0  30979  signshlen  30992  signshnz  30993  elmrsubrn  31740  lswn0  41955  pfxid  41967  addlenrevpfx  41972  addlenpfx  41973  pfxtrcfv0  41977  pfxeq  41979  pfxtrcfvl  41980  pfxsuffeqwrdeq  41981  pfxccat1  41985  pfx2  41987  pfxcctswrd  41992  ccats1pfxeq  41996  ccats1pfxeqrex  41997  pfxccatin12lem2  41999  pfxccatin12  42000  pfxccat3  42001  pfxccatpfx2  42003  pfxccat3a  42004  pfxccatid  42005  ccats1pfxeqbi  42006
  Copyright terms: Public domain W3C validator