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

Theorem lencl 13356
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 13355 . 2 (𝑊 ∈ Word 𝑆𝑊 ∈ Fin)
2 hashcl 13185 . 2 (𝑊 ∈ Fin → (#‘𝑊) ∈ ℕ0)
31, 2syl 17 1 (𝑊 ∈ Word 𝑆 → (#‘𝑊) ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cfv 5926  Fincfn 7997  0cn0 11330  #chash 13157  Word cword 13323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-hash 13158  df-word 13331
This theorem is referenced by:  wrdffz  13358  wrdsymb0  13371  wrdlenge1n0  13372  wrdlenge2n0  13374  wrdsymb1  13375  eqwrd  13379  wrdred1  13382  wrdred1hash  13383  ccatcl  13392  ccatlen  13393  ccat0  13394  ccatval1  13395  ccatval3  13397  elfzelfzccat  13398  ccatsymb  13400  ccatfv0  13401  ccatval21sw  13403  ccatlid  13404  ccatrid  13405  ccatass  13406  ccatrn  13407  lswccatn0lsw  13409  ccatalpha  13411  ccatws1lenp1b  13439  wrdlenccats1lenm1  13440  wrdlenccats1lenm1OLD  13441  ccatw2s1len  13444  ccatw2s1lenOLD  13445  ccats1val2  13447  ccat1st1st  13448  ccatws1lenrevOLD  13452  ccatws1n0  13453  ccatws1n0OLD  13454  lswccats1fst  13457  ccatw2s1p1  13458  ccat2s1fvw  13460  swrdid  13474  swrdn0  13476  swrdnd  13478  swrdnd2  13479  swrdrlen  13481  addlenrevswrd  13483  addlenswrd  13484  swrdtrcfv0  13488  swrdeq  13490  swrdlen2  13491  swrdfv2  13492  swrdtrcfvl  13496  swrdlsw  13498  2swrdeqwrdeq  13499  2swrd1eqwrdeq  13500  swrdccat1  13503  swrdccat2  13504  wrdcctswrd  13511  ccats1swrdeq  13515  ccatopth2  13517  cats1un  13521  wrdind  13522  wrd2ind  13523  ccats1swrdeqrex  13524  swrdccatin1  13529  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12lem3  13536  swrdccatin12  13537  swrdccat3  13538  swrdccat  13539  swrdccat3a  13540  swrdccat3blem  13541  swrdccat3b  13542  swrdccatid  13543  ccats1swrdeqbi  13544  spllen  13551  splval2  13554  revcl  13556  revlen  13557  revccat  13561  revrev  13562  repswsymball  13572  repswsymballbi  13573  cshwsublen  13588  cshwn  13589  cshwlen  13591  cshwidxmod  13595  2cshwid  13606  3cshw  13610  cshweqdif2  13611  cshw1  13614  scshwfzeqfzo  13618  revco  13626  ccatco  13627  cats1fvn  13649  cats1fv  13650  swrd2lsw  13741  2swrd2eqwrdeq  13742  ccat2s1fvwALT  13744  cshwshashnsame  15857  gsmsymgrfixlem1  17893  gsmsymgreqlem2  17897  pmtrdifwrdellem2  17948  psgnuni  17965  psgnran  17981  efginvrel2  18186  efgsdmi  18191  efgsval2  18192  efgsp1  18196  efgsfo  18198  efgredlemf  18200  efgredlemg  18201  efgredleme  18202  efgredlemd  18203  efgredlemc  18204  efgredlem  18206  efgred  18207  efgcpbllemb  18214  frgpuplem  18231  frgpnabllem1  18322  pgpfaclem1  18526  psgnghm  19974  upgrewlkle2  26558  wlkcl  26567  wlkeq  26585  wlkv0  26603  wlklenvclwlk  26607  redwlklem  26624  wlkp1lem3  26628  wlkp1lem8  26633  wlkdlem1  26635  pthdlem1  26718  pthdlem2  26720  wlkiswwlks1  26821  wlkiswwlks2lem1  26823  wlkiswwlks2lem3  26825  wlkiswwlks2lem4  26826  wwlksm1edg  26835  wlklnwwlkln2lem  26836  wwlksnextbi  26857  wwlksnextproplem2  26873  wwlksnextproplem3  26874  rusgrnumwwlks  26941  umgrclwwlkge2  26957  clwlkclwwlklem2a1  26958  clwlkclwwlklem2a2  26959  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwlkclwwlklem3  26967  clwlkclwwlk  26968  clwlkclwwlk2  26969  clwwisshclwwslem  26971  erclwwlkref  26977  clwwlkn  26985  clwwlkwwlksb  27018  clwlksfclwwlk2wrd  27045  clwlksfclwwlk1hash  27047  clwlksfclwwlk  27049  clwlksf1clwwlklem1  27052  clwlksf1clwwlklem3  27054  clwwlknonex2lem2  27083  eupth2eucrct  27195  eucrctshift  27221  clwwlkccatlem  27331  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  sseqfv1  30579  sseqfn  30580  sseqmw  30581  sseqf  30582  sseqfv2  30584  sseqp1  30585  signstlen  30772  signstfvn  30774  signstfvp  30776  signstfvneq0  30777  signstfvc  30779  signstfveq0a  30781  signstfveq0  30782  signshlen  30795  signshnz  30796  elmrsubrn  31543  lswn0  41705  pfxid  41717  addlenrevpfx  41722  addlenpfx  41723  pfxtrcfv0  41727  pfxeq  41729  pfxtrcfvl  41730  pfxsuffeqwrdeq  41731  pfxccat1  41735  pfx2  41737  pfxcctswrd  41742  ccats1pfxeq  41746  ccats1pfxeqrex  41747  pfxccatin12lem2  41749  pfxccatin12  41750  pfxccat3  41751  pfxccatpfx2  41753  pfxccat3a  41754  pfxccatid  41755  ccats1pfxeqbi  41756
  Copyright terms: Public domain W3C validator