Theorem wrdf 14490

Description: A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)

Assertion

Ref	Expression
wrdf	⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Proof of Theorem wrdf

Dummy variable 𝑙 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iswrd 14487	. 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆)
2		simpr 484	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆)
3		fnfzo0hash 14422	. . . . . 6 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙)
4	3	oveq2d 7406	. . . . 5 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙))
5	4	feq2d 6675	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0..^𝑙)⟶𝑆))
6	2, 5	mpbird 257	. . 3 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
7	6	rexlimiva 3127	. 2 ⊢ (∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
8	1, 7	sylbi 217	1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3054  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390  0cc0 11075  ℕ₀cn0 12449  ..^cfzo 13622  ♯chash 14302  Word cword 14485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-card 9899  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537  df-uz 12801  df-fz 13476  df-fzo 13623  df-hash 14303  df-word 14486

This theorem is referenced by:  wrdfd  14491  iswrdb  14492  wrddm  14493  wrdsymbcl  14499  wrdfn  14500  wrdffz  14507  0wrd0  14512  wrdsymb  14514  wrdnval  14517  wrdred1  14532  wrdred1hash  14533  ccatcl  14546  ccatalpha  14565  s1dm  14580  swrdcl  14617  swrdf  14622  swrdwrdsymb  14634  pfxres  14651  cats1un  14693  revcl  14733  revlen  14734  revrev  14739  repsdf2  14750  cshwf  14772  cshinj  14783  wrdco  14804  lenco  14805  revco  14807  ccatco  14808  lswco  14812  s2dm  14863  wwlktovf  14929  s7f1o  14939  ofccat  14942  gsumwsubmcl  18771  gsumsgrpccat  18774  gsumwmhm  18779  frmdss2  18797  symgtrinv  19409  psgnunilem5  19431  psgnunilem2  19432  psgnunilem3  19433  efginvrel1  19665  efgsf  19666  efgsrel  19671  efgs1b  19673  efgredlemf  19678  efgredlemd  19681  efgredlemc  19682  efgredlem  19684  frgpup3lem  19714  pgpfaclem1  20020  ablfaclem2  20025  ablfaclem3  20026  ablfac2  20028  dchrptlem1  27182  dchrptlem2  27183  trgcgrg  28449  tgcgr4  28465  wrdupgr  29019  wrdumgr  29031  vdegp1ai  29471  vdegp1bi  29472  wlkres  29605  wlkp1  29616  wlkdlem1  29617  trlf1  29633  trlreslem  29634  upgrwlkdvdelem  29673  pthdlem1  29703  pthdlem2lem  29704  uspgrn2crct  29745  wlkiswwlks2lem3  29808  wlkiswwlksupgr2  29814  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  1wlkdlem1  30073  wlk2v2e  30093  eucrctshift  30179  konigsbergssiedgw  30186  wrdres  32863  pfxf1  32870  s3f1  32875  ccatf1  32877  swrdrn3  32884  cycpmcl  33080  tocyc01  33082  cycpmco2rn  33089  cycpmrn  33107  tocyccntz  33108  cycpmconjslem2  33119  unitprodclb  33367  sseqf  34390  fiblem  34396  ofcccat  34541  signstcl  34563  signstf  34564  signstfvn  34567  signsvtn0  34568  signstres  34573  signsvtp  34581  signsvtn  34582  signsvfpn  34583  signsvfnn  34584  signshf  34586  revwlk  35119  mvrsfpw  35500  frlmfzowrdb  42499  amgm2d  44194  amgm3d  44195  amgm4d  44196  lswn0  47449  upgrimwlklem1  47901  upgrimwlklem2  47902  upgrimwlklem3  47903  upgrimtrlslem1  47908  upgrimtrlslem2  47909  gpgprismgr4cycllem9  48097  amgmw2d  49797