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

Theorem lencl 13128
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 13127 . 2 (𝑊 ∈ Word 𝑆𝑊 ∈ Fin)
2 hashcl 12964 . 2 (𝑊 ∈ Fin → (#‘𝑊) ∈ ℕ0)
31, 2syl 17 1 (𝑊 ∈ Word 𝑆 → (#‘𝑊) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cfv 5790  Fincfn 7819  0cn0 11142  #chash 12937  Word cword 13095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-oadd 7429  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-card 8626  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-nn 10871  df-n0 11143  df-z 11214  df-uz 11523  df-fz 12156  df-fzo 12293  df-hash 12938  df-word 13103
This theorem is referenced by:  wrdffz  13130  wrdsymb0  13143  wrdlenge1n0  13144  wrdlenge2n0  13145  wrdsymb1  13146  eqwrd  13150  ccatcl  13161  ccatlen  13162  ccatval1  13163  ccatval3  13165  elfzelfzccat  13166  ccatsymb  13168  ccatfv0  13169  ccatlid  13171  ccatrid  13172  ccatass  13173  ccatrn  13174  lswccatn0lsw  13175  ccatalpha  13177  wrdlenccats1lenm1  13201  ccatw2s1len  13203  ccats1val2  13205  ccatws1lenrev  13209  ccatws1n0  13210  lswccats1fst  13213  ccatw2s1p1  13214  ccat2s1fvw  13216  swrdid  13229  swrdn0  13231  swrdnd  13233  swrdnd2  13234  swrdrlen  13236  addlenrevswrd  13238  addlenswrd  13239  swrdtrcfv0  13243  swrdeq  13245  swrdlen2  13246  swrdfv2  13247  swrdtrcfvl  13251  swrdlsw  13253  2swrdeqwrdeq  13254  2swrd1eqwrdeq  13255  swrdccat1  13258  swrdccat2  13259  wrdcctswrd  13266  ccats1swrdeq  13270  ccatopth2  13272  cats1un  13276  wrdind  13277  wrd2ind  13278  ccats1swrdeqrex  13279  swrdccatin1  13283  swrdccatin2  13287  swrdccatin12lem2  13289  swrdccatin12lem3  13290  swrdccatin12  13291  swrdccat3  13292  swrdccat  13293  swrdccat3a  13294  swrdccat3blem  13295  swrdccat3b  13296  swrdccatid  13297  ccats1swrdeqbi  13298  spllen  13305  splval2  13308  revcl  13310  revlen  13311  revccat  13315  revrev  13316  repswsymball  13326  repswsymballbi  13327  cshwsublen  13342  cshwn  13343  cshwlen  13345  cshwidxmod  13349  2cshwid  13360  3cshw  13364  cshweqdif2  13365  cshw1  13368  scshwfzeqfzo  13372  revco  13380  ccatco  13381  cats1fvn  13403  cats1fv  13404  swrd2lsw  13492  2swrd2eqwrdeq  13493  ccat2s1fvwALT  13495  cshwshashnsame  15597  gsmsymgrfixlem1  17619  gsmsymgreqlem2  17623  pmtrdifwrdellem2  17674  psgnuni  17691  psgnran  17707  efginvrel2  17912  efgsdmi  17917  efgsval2  17918  efgsp1  17922  efgsfo  17924  efgredlemf  17926  efgredlemg  17927  efgredleme  17928  efgredlemd  17929  efgredlemc  17930  efgredlem  17932  efgred  17933  efgcpbllemb  17940  frgpuplem  17957  frgpnabllem1  18048  pgpfaclem1  18252  psgnghm  19693  wlkbprop  25845  wlkn0  25849  wlklenvm1  25854  wlkonwlk  25859  pthdepisspth  25898  spthonepeq  25911  redwlklem  25929  nvnencycllem  25965  wlkiswwlk1  26012  wlkiswwlk2lem1  26013  wlkiswwlk2lem3  26015  wlkiswwlk2lem4  26016  wlklniswwlkn2  26022  2wlkeq  26029  wwlknextbi  26047  wwlkm1edg  26057  wwlkextproplem2  26064  wwlkextproplem3  26065  wlkv0  26082  clwwlkgt0  26093  clwwlknprop  26094  clwwlkn0  26096  clwlkisclwwlklem2a1  26101  clwlkisclwwlklem2a2  26102  clwlkisclwwlklem2a4  26106  clwlkisclwwlklem2a  26107  clwlkisclwwlklem1  26109  clwlkisclwwlklem0  26110  clwlkisclwwlk  26111  clwlkisclwwlk2  26112  clwwisshclwwlem  26128  erclwwlkref  26135  wlklenvp1  26159  wlklenvclwlk  26160  clwlkfclwwlk2wrd  26161  clwlkfclwwlk1hash  26163  clwlkfclwwlk  26165  clwlkf1clwwlklem1  26167  clwlkf1clwwlklem3  26169  rusgranumwlks  26277  numclwwlkovf2ex  26407  numclwlk2lem2f1o  26426  sseqfv1  29612  sseqfn  29613  sseqmw  29614  sseqf  29615  sseqfv2  29617  sseqp1  29618  signstlen  29804  signstfvn  29806  signstfvp  29808  signstfvneq0  29809  signstfvc  29811  signstfveq0a  29813  signstfveq0  29814  signshlen  29827  signshnz  29828  elmrsubrn  30505  wrdred1  40065  wrdred1hash  40066  lswn0  40067  pfxid  40080  addlenrevpfx  40085  addlenpfx  40086  pfxtrcfv0  40090  pfxeq  40092  pfxtrcfvl  40093  pfxsuffeqwrdeq  40094  pfxccat1  40098  pfx2  40100  pfxcctswrd  40105  ccats1pfxeq  40109  ccats1pfxeqrex  40110  pfxccatin12lem2  40112  pfxccatin12  40113  pfxccat3  40114  pfxccatpfx2  40116  pfxccat3a  40117  pfxccatid  40118  ccats1pfxeqbi  40119  upgrewlkle2  40830  1wlkcl  40842  1wlkeq  40860  1wlkv0  40881  1wlklenvclwlk  40885  red1wlklem  40902  1wlkp1lem3  40906  1wlkp1lem8  40911  1wlkdlem1  40913  pthdlem1  40994  pthdlem2  40996  1wlkiswwlks1  41086  1wlkiswwlks2lem1  41088  1wlkiswwlks2lem3  41090  1wlkiswwlks2lem4  41091  wwlksm1edg  41100  1wlklnwwlkln2lem  41101  wwlksnextbi  41122  wwlksnextproplem2  41138  wwlksnextproplem3  41139  rusgrnumwwlks  41199  clwlkclwwlklem2a1  41223  clwlkclwwlklem2a2  41224  clwlkclwwlklem2a4  41228  clwlkclwwlklem2a  41229  clwlkclwwlklem2  41231  clwlkclwwlklem3  41232  clwlkclwwlk  41233  clwlkclwwlk2  41234  umgrclwwlksge2  41241  clwwisshclwwslem  41256  erclwwlksref  41263  clwlksfclwwlk2wrd  41287  clwlksfclwwlk1hash  41289  clwlksfclwwlk  41291  clwlksf1clwwlklem1  41294  clwlksf1clwwlklem3  41296  eupth2eucrct  41407  eucrctshift  41433  av-numclwwlkovf2ex  41539  av-numclwlk2lem2f1o  41557
  Copyright terms: Public domain W3C validator