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

Theorem lencl 12543
Description: The length of a word is a nonnegative integer. (Contributed by Stefan O'Rear, 27-Aug-2015.)
Assertion
Ref Expression
lencl  |-  ( W  e. Word  S  ->  ( # `
 W )  e. 
NN0 )

Proof of Theorem lencl
StepHypRef Expression
1 wrdfin 12542 . 2  |-  ( W  e. Word  S  ->  W  e.  Fin )
2 hashcl 12409 . 2  |-  ( W  e.  Fin  ->  ( # `
 W )  e. 
NN0 )
31, 2syl 16 1  |-  ( W  e. Word  S  ->  ( # `
 W )  e. 
NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   ` cfv 5578   Fincfn 7518   NN0cn0 10802   #chash 12386  Word cword 12515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-card 8323  df-cda 8551  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544  df-2 10601  df-n0 10803  df-z 10872  df-uz 11092  df-fz 11683  df-fzo 11806  df-hash 12387  df-word 12523
This theorem is referenced by:  wrdsymb0  12556  wrdlenge1n0  12557  wrdlenge2n0  12558  wrdsymb1  12559  eqwrd  12563  lsw0  12567  lswcl  12570  ccatlen  12575  ccatval3  12578  elfzelfzccat  12579  ccatsymb  12581  ccatfv0  12582  ccatval1lsw  12583  ccatlid  12584  ccatrid  12585  ccatass  12586  ccatrn  12587  lswccatn0lsw  12588  lswccat0lsw  12589  wrdlenccats1lenm1  12608  ccatw2s1len  12610  ccats1val2  12612  ccatws1lenrev  12616  ccatws1n0  12617  lswccats1fst  12620  ccatw2s1p1  12621  ccatw2s1p2  12622  ccat2s1fvw  12623  swrdid  12633  swrdn0  12636  swrdnd  12638  swrdrlen  12640  addlenrevswrd  12642  addlenswrd  12643  swrdvalodm2  12645  swrdvalodm  12646  swrdtrcfv0  12650  swrdeq  12652  swrdsymbeq  12653  swrdspsleq  12654  wrdeqswrdlsw  12655  swrdtrcfvl  12656  swrdlsw  12658  2swrdeqwrdeq  12659  2swrd1eqwrdeq  12660  swrdccat1  12663  swrdccat2  12664  wrdcctswrd  12671  ccats1swrdeq  12675  ccatopth2  12677  cats1un  12682  wrdind  12683  wrd2ind  12684  ccats1swrdeqrex  12685  swrdccatin1  12689  swrdccatin2  12693  swrdccatin12lem2  12695  swrdccatin12lem3  12696  swrdccatin12  12697  swrdccat3  12698  swrdccat  12699  swrdccat3a  12700  swrdccat3blem  12701  swrdccat3b  12702  swrdccatid  12703  ccats1swrdeqbi  12704  spllen  12711  splval2  12714  revcl  12716  revlen  12717  revccat  12721  revrev  12722  repswsymball  12732  repswsymballbi  12733  cshwsublen  12748  cshwn  12749  cshwlen  12751  cshwidxmod  12755  2cshwid  12763  3cshw  12767  cshweqdif2  12768  cshw1  12771  scshwfzeqfzo  12775  revco  12781  ccatco  12782  cats1fvn  12804  cats1fv  12805  swrd2lsw  12871  2swrd2eqwrdeq  12872  ccat2s1fvwALT  12874  cshwshashnsame  14569  gsmsymgrfixlem1  16430  gsmsymgreqlem2  16434  pmtrdifwrdellem2  16485  psgnuni  16502  psgnran  16518  efginvrel2  16723  efgsdmi  16728  efgsval2  16729  efgsp1  16733  efgsfo  16735  efgredlemf  16737  efgredlemg  16738  efgredleme  16739  efgredlemd  16740  efgredlemc  16741  efgredlem  16743  efgred  16744  efgcpbllemb  16751  frgpuplem  16768  frgpnabllem1  16855  pgpfaclem1  17110  psgnghm  18593  wlkbprop  24499  wlkn0  24503  wlklenvm1  24508  wlkonwlk  24513  pthdepisspth  24552  spthonepeq  24565  redwlklem  24583  nvnencycllem  24619  wlkiswwlk1  24666  wlkiswwlk2lem1  24667  wlkiswwlk2lem3  24669  wlkiswwlk2lem4  24670  wlklniswwlkn2  24676  2wlkeq  24683  wwlknextbi  24701  wwlkm1edg  24711  wwlkextproplem2  24718  wwlkextproplem3  24719  wlkv0  24736  clwwlkgt0  24747  clwwlknprop  24748  clwwlkn0  24750  clwlkisclwwlklem2a1  24755  clwlkisclwwlklem2a2  24756  clwlkisclwwlklem2a4  24760  clwlkisclwwlklem2a  24761  clwlkisclwwlklem1  24763  clwlkisclwwlklem0  24764  clwlkisclwwlk  24765  clwlkisclwwlk2  24766  clwwisshclwwlem  24782  erclwwlkref  24789  wlklenvp1  24814  wlklenvclwlk  24815  clwlkfclwwlk2wrd  24816  clwlkfclwwlk1hash  24818  clwlkfclwwlk  24820  clwlkf1clwwlklem1  24822  clwlkf1clwwlklem3  24824  rusgranumwlks  24932  numclwwlkovf2ex  25062  numclwlk2lem2f1o  25081  sseqfv1  28305  sseqfn  28306  sseqmw  28307  sseqf  28308  sseqfv2  28310  sseqp1  28311  signstlen  28501  signstfvn  28503  signstfvp  28505  signstfvneq0  28506  signstfvc  28508  signstfveq0a  28510  signstfveq0  28511  signshlen  28524  signshnz  28525  elmrsubrn  28857  lswn0  32181
  Copyright terms: Public domain W3C validator