Theorem wrdf 14471

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 14468	. 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆)
2		simpr 484	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆)
3		fnfzo0hash 14403	. . . . . 6 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙)
4	3	oveq2d 7376	. . . . 5 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙))
5	4	feq2d 6646	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0..^𝑙)⟶𝑆))
6	2, 5	mpbird 257	. . 3 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
7	6	rexlimiva 3131	. 2 ⊢ (∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
8	1, 7	sylbi 217	1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062  ⟶wf 6488  ‘cfv 6492  (class class class)co 7360  0cc0 11029  ℕ₀cn0 12428  ..^cfzo 13599  ♯chash 14283  Word cword 14466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780  df-fz 13453  df-fzo 13600  df-hash 14284  df-word 14467

This theorem is referenced by:  wrdfd  14472  iswrdb  14473  wrddm  14474  wrdsymbcl  14480  wrdfn  14481  wrdffz  14488  0wrd0  14493  wrdsymb  14495  wrdnval  14498  wrdred1  14513  wrdred1hash  14514  ccatcl  14527  ccatalpha  14547  s1dm  14562  swrdcl  14599  swrdf  14604  swrdwrdsymb  14616  pfxres  14633  cats1un  14674  revcl  14714  revlen  14715  revrev  14720  repsdf2  14731  cshwf  14753  cshinj  14764  wrdco  14784  lenco  14785  revco  14787  ccatco  14788  lswco  14792  s2dm  14843  wwlktovf  14909  s7f1o  14919  ofccat  14922  chnf  18586  gsumwsubmcl  18796  gsumsgrpccat  18799  gsumwmhm  18804  frmdss2  18822  symgtrinv  19438  psgnunilem5  19460  psgnunilem2  19461  psgnunilem3  19462  efginvrel1  19694  efgsf  19695  efgsrel  19700  efgs1b  19702  efgredlemf  19707  efgredlemd  19710  efgredlemc  19711  efgredlem  19713  frgpup3lem  19743  pgpfaclem1  20049  ablfaclem2  20054  ablfaclem3  20055  ablfac2  20057  dchrptlem1  27241  dchrptlem2  27242  trgcgrg  28597  tgcgr4  28613  wrdupgr  29168  wrdumgr  29180  vdegp1ai  29620  vdegp1bi  29621  wlkres  29752  wlkp1  29763  wlkdlem1  29764  trlf1  29780  trlreslem  29781  upgrwlkdvdelem  29819  pthdlem1  29849  pthdlem2lem  29850  uspgrn2crct  29891  wlkiswwlks2lem3  29954  wlkiswwlksupgr2  29960  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  1wlkdlem1  30222  wlk2v2e  30242  eucrctshift  30328  konigsbergssiedgw  30335  wrdres  33010  pfxf1  33017  s3f1  33022  ccatf1  33024  swrdrn3  33030  cycpmcl  33192  tocyc01  33194  cycpmco2rn  33201  cycpmrn  33219  tocyccntz  33220  cycpmconjslem2  33231  unitprodclb  33464  sseqf  34552  fiblem  34558  ofcccat  34703  signstcl  34725  signstf  34726  signstfvn  34729  signsvtn0  34730  signstres  34735  signsvtp  34743  signsvtn  34744  signsvfpn  34745  signsvfnn  34746  signshf  34748  revwlk  35323  mvrsfpw  35704  frlmfzowrdb  42963  amgm2d  44643  amgm3d  44644  amgm4d  44645  chnsubseqword  47324  chnsubseqwl  47325  chnsubseq  47326  lswn0  47916  upgrimwlklem1  48385  upgrimwlklem2  48386  upgrimwlklem3  48387  upgrimtrlslem1  48392  upgrimtrlslem2  48393  gpgprismgr4cycllem9  48591  amgmw2d  50291