Theorem lencl 14581

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6573  Fincfn 9003  ℕ₀cn0 12553  ♯chash 14379  Word cword 14562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640  df-uz 12904  df-fz 13568  df-fzo 13712  df-hash 14380  df-word 14563

This theorem is referenced by:  wrdffz  14583  wrdnfi  14596  wrdsymb0  14597  wrdlenge1n0  14598  wrdlenge2n0  14600  wrdsymb1  14601  eqwrd  14605  wrdred1  14608  wrdred1hash  14609  ccatcl  14622  ccatlen  14623  ccat0  14624  ccatval1  14625  ccatval3  14627  elfzelfzccat  14628  ccatsymb  14630  ccatfv0  14631  ccatval21sw  14633  ccatlid  14634  ccatrid  14635  ccatass  14636  ccatrn  14637  lswccatn0lsw  14639  ccatalpha  14641  ccatws1lenp1b  14669  wrdlenccats1lenm1  14670  ccatw2s1len  14673  ccats1val2  14675  ccatws1n0  14680  lswccats1fst  14683  ccatw2s1p1  14684  ccat2s1fvw  14686  swrdnd  14702  swrdnd2  14703  swrdnd0  14705  swrdrlen  14707  swrdlen2  14708  swrdfv2  14709  swrdlsw  14715  swrdccat2  14717  pfxid  14732  pfxn0  14734  pfxnd0  14736  addlenrevpfx  14738  addlenpfx  14739  pfxtrcfv0  14742  pfxeq  14744  pfxtrcfvl  14745  pfxsuffeqwrdeq  14746  pfxccat1  14750  pfxcctswrd  14758  ccats1pfxeq  14762  ccats1pfxeqrex  14763  ccatopth2  14765  cats1un  14769  wrdind  14770  wrd2ind  14771  swrdccatin1  14773  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12lem3  14780  pfxccatin12  14781  pfxccat3  14782  swrdccat  14783  pfxccatpfx2  14785  pfxccat3a  14786  swrdccat3blem  14787  swrdccat3b  14788  pfxccatid  14789  ccats1pfxeqbi  14790  spllen  14802  splfv1  14803  splfv2a  14804  splval2  14805  revcl  14809  revlen  14810  revccat  14814  revrev  14815  repswsymball  14827  repswsymballbi  14828  cshw0  14842  cshwsublen  14844  cshwn  14845  cshwlen  14847  cshwidxmod  14851  2cshwid  14862  3cshw  14866  cshweqdif2  14867  cshw1  14870  scshwfzeqfzo  14875  revco  14883  ccatco  14884  cats1fvn  14907  cats1fv  14908  pfx2  14996  swrd2lsw  15001  2swrd2eqwrdeq  15002  ccat2s1fvwALT  15004  cshwshashnsame  17151  gsmsymgrfixlem1  19469  gsmsymgreqlem2  19473  pmtrdifwrdellem2  19524  psgnuni  19541  psgnran  19557  efginvrel2  19769  efgsdmi  19774  efgsval2  19775  efgsp1  19779  efgsfo  19781  efgredlemf  19783  efgredlemg  19784  efgredleme  19785  efgredlemd  19786  efgredlemc  19787  efgredlem  19789  efgred  19790  efgcpbllemb  19797  frgpuplem  19814  frgpnabllem1  19915  pgpfaclem1  20125  psgnghm  21621  upgrewlkle2  29642  wlkcl  29651  wlkeq  29670  wlkv0  29687  wlklenvclwlk  29691  redwlklem  29707  wlkp1lem3  29711  wlkp1lem8  29716  wlkdlem1  29718  pthdlem1  29802  pthdlem2  29804  wlkiswwlks1  29900  wlkiswwlks2lem1  29902  wlkiswwlks2lem3  29904  wlkiswwlks2lem4  29905  wwlksm1edg  29914  wlklnwwlkln2lem  29915  wwlksnextbi  29927  wwlksnextproplem2  29943  wwlksnextproplem3  29944  rusgrnumwwlks  30007  clwwlkccatlem  30021  umgrclwwlkge2  30023  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a2  30025  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlklem3  30033  clwlkclwwlk  30034  clwlkclwwlk2  30035  clwlkclwwlkfo  30041  clwwisshclwwslem  30046  erclwwlkref  30052  clwwlkn  30058  clwwlkwwlksb  30086  clwlknf1oclwwlknlem1  30113  clwwlknonex2lem2  30140  eupth2eucrct  30249  eucrctshift  30275  numclwlk2lem2f1o  30411  ccatf1  32915  ccatdmss  32916  pfxlsw2ccat  32917  ccatws1f1o  32918  ccatws1f1olast  32919  wrdt2ind  32920  splfv3  32925  chnind  32983  chnub  32984  chnlt  32985  cycpmfv1  33106  cycpmfv2  33107  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  cycpmrn  33136  cyc3genpm  33145  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  dfufd2lem  33542  sseqfv1  34354  sseqfn  34355  sseqmw  34356  sseqf  34357  sseqfv2  34359  sseqp1  34360  ofcccat  34520  signstlen  34544  signstfvn  34546  signstfvp  34548  signstfvneq0  34549  signstfvc  34551  signstfveq0a  34553  signstfveq0  34554  signshf  34565  signshlen  34567  signshnz  34568  lpadlem3  34655  lpadlem2  34657  lpadlen2  34658  lpadmax  34659  lpadleft  34660  lpadright  34661  revpfxsfxrev  35083  revwlk  35092  elmrsubrn  35488  ccatcan2d  42246  lswn0  47318