Theorem lencl 11232

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

Dummy variable 𝑙 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iswrd 11230	. . 3 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆)
2	1	biimpi 120	. 2 ⊢ (𝑊 ∈ Word 𝑆 → ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆)
3		fnfzo0hash 11206	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙)
4	3	adantl 277	. . 3 ⊢ ((𝑊 ∈ Word 𝑆 ∧ (𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆)) → (♯‘𝑊) = 𝑙)
5		simprl 531	. . 3 ⊢ ((𝑊 ∈ Word 𝑆 ∧ (𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆)) → 𝑙 ∈ ℕ0)
6	4, 5	eqeltrd 2311	. 2 ⊢ ((𝑊 ∈ Word 𝑆 ∧ (𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆)) → (♯‘𝑊) ∈ ℕ0)
7	2, 6	rexlimddv 2667	1 ⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ0)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2205  ∃wrex 2523  ⟶wf 5350  ‘cfv 5354  (class class class)co 6052  0cc0 8129  ℕ₀cn0 9498  ..^cfzo 10480  ♯chash 11142  Word cword 11228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-coll 4227  ax-sep 4230  ax-nul 4238  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-iinf 4712  ax-cnex 8220  ax-resscn 8221  ax-1cn 8222  ax-1re 8223  ax-icn 8224  ax-addcl 8225  ax-addrcl 8226  ax-mulcl 8227  ax-addcom 8229  ax-addass 8231  ax-distr 8233  ax-i2m1 8234  ax-0lt1 8235  ax-0id 8237  ax-rnegex 8238  ax-cnre 8240  ax-pre-ltirr 8241  ax-pre-ltwlin 8242  ax-pre-lttrn 8243  ax-pre-apti 8244  ax-pre-ltadd 8245

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3045  df-csb 3141  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-nul 3511  df-if 3623  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-int 3952  df-iun 3995  df-br 4112  df-opab 4174  df-mpt 4175  df-tr 4211  df-id 4416  df-iord 4489  df-on 4491  df-ilim 4492  df-suc 4494  df-iom 4715  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-res 4763  df-ima 4764  df-iota 5314  df-fun 5356  df-fn 5357  df-f 5358  df-f1 5359  df-fo 5360  df-f1o 5361  df-fv 5362  df-riota 6005  df-ov 6055  df-oprab 6056  df-mpo 6057  df-1st 6336  df-2nd 6337  df-recs 6538  df-frec 6624  df-1o 6649  df-er 6769  df-en 6978  df-dom 6979  df-fin 6980  df-pnf 8312  df-mnf 8313  df-xr 8314  df-ltxr 8315  df-le 8316  df-sub 8448  df-neg 8449  df-inn 9240  df-n0 9499  df-z 9580  df-uz 9857  df-fz 10346  df-fzo 10481  df-ihash 11143  df-word 11229

This theorem is referenced by:  iswrdsymb  11246  wrdfin  11247  wrdffz  11249  wrdsymb  11256  wrdsymb0  11261  wrdlenge1n0  11262  wrdlenge2n0  11264  wrdsymb1  11265  eqwrd  11269  wrdred1  11271  wrdred1hash  11272  lswwrd  11275  ccatcl  11285  ccatlen  11287  ccat0  11288  ccatval1  11289  ccatval2  11290  ccatval3  11291  elfzelfzccat  11292  ccatvalfn  11293  ccatsymb  11294  ccatfv0  11295  ccatval21sw  11297  ccatlid  11298  ccatrid  11299  ccatass  11300  ccatrn  11301  lswccatn0lsw  11303  ccatalpha  11305  ccatws1lenp1bg  11327  wrdlenccats1lenm1g  11328  ccatw2s1leng  11330  ccats1val2  11332  ccat1st1st  11333  lswccats1  11335  lswccats1fst  11336  ccatw2s1p1g  11337  ccat2s1fvwd  11339  fzowrddc  11343  swrdnd  11355  swrdrlen  11357  swrdlen2  11358  swrdfv2  11359  swrdlsw  11365  swrdccat2  11367  pfxid  11382  pfxn0  11384  pfxwrdsymbg  11386  addlenpfx  11387  pfxtrcfv0  11390  pfxeq  11392  pfxtrcfvl  11393  pfxsuffeqwrdeq  11394  pfxccat1  11398  pfxcctswrd  11406  lenrevpfxcctswrd  11408  ccats1pfxeq  11410  ccats1pfxeqrex  11411  ccatopth2  11413  cats1un  11417  wrdind  11418  wrd2ind  11419  swrdccatin1  11421  swrdccatin2  11425  pfxccatin12lem2  11427  pfxccatin12lem3  11428  pfxccatin12  11429  pfxccat3  11430  swrdccat  11431  pfxccatpfx2  11433  pfxccat3a  11434  swrdccat3blem  11435  swrdccat3b  11436  pfxccatid  11437  ccats1pfxeqbi  11438  cats1fvn  11460  cats1fvnd  11461  cats1fvd  11462  wrdupgren  16108  wrdumgren  16118  vdegp1aid  16326  vdegp1bid  16327  wksfval  16334  wlkex  16337  iswlkg  16341  wlkcl  16344  wlkclg  16345  wlkeq  16366  wlkv0  16381  wlklenvclwlk  16385  clwwlkccatlem  16412  umgrclwwlkge2  16414  isclwwlkn  16425  clwwlknonex2lem2  16450  konigsbergssiedgwen  16498  konigsberglem5  16504