Theorem wrdf 14575

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 14572	. 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆)
2		simpr 490	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆)
3		fnfzo0hash 14507	. . . . . 6 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙)
4	3	oveq2d 7439	. . . . 5 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙))
5	4	feq2d 6696	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0..^𝑙)⟶𝑆))
6	2, 5	mpbird 260	. . 3 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
7	6	rexlimiva 3161	. 2 ⊢ (∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
8	1, 7	sylbi 220	1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∃wrex 3092  ⟶wf 6539  ‘cfv 6543  (class class class)co 7423  0cc0 11118  ℕ₀cn0 12522  ..^cfzo 13701  ♯chash 14386  Word cword 14570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-int 4918  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-card 9944  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-nn 12252  df-n0 12523  df-z 12610  df-uz 12881  df-fz 13554  df-fzo 13702  df-hash 14387  df-word 14571

This theorem is used by:  wrdfd  14576  iswrdb  14577  wrddm  14578  wrdsymbcl  14584  wrdfn  14585  wrdffz  14592  0wrd0  14597  wrdsymb  14599  wrdnval  14602  wrdred1  14617  wrdred1hash  14618  ccatcl  14631  ccatf1  14648  ccatalpha  14652  s1dm  14667  swrdcl  14705  swrdf  14710  swrdrn3  14714  swrdwrdsymb  14724  pfxres  14741  cats1un  14782  revcl  14822  revlen  14823  revrev  14828  repsdf2  14841  cshwf  14863  cshinj  14874  wrdco  14894  lenco  14895  revco  14897  ccatco  14898  lswco  14902  s2dm  14953  wwlktovf  15019  s7f1o  15029  ofccat  15032  chnf  18710  gsumwsubmcl  18927  gsumsgrpccat  18930  gsumwmhm  18935  frmdss2  18953  symgtrinv  19573  psgnunilem5  19595  psgnunilem2  19596  psgnunilem3  19597  efginvrel1  19829  efgsf  19830  efgsrel  19835  efgs1b  19837  efgredlemf  19842  efgredlemd  19845  efgredlemc  19846  efgredlem  19848  frgpup3lem  19878  pgpfaclem1  20184  ablfaclem2  20189  ablfaclem3  20190  ablfac2  20192  dchrptlem1  27465  dchrptlem2  27466  trgcgrg  28821  tgcgr4  28837  wrdupgr  29472  wrdumgr  29484  vdegp1ai  29923  vdegp1bi  29924  wlkres  30055  wlkp1  30066  wlkdlem1  30067  trlf1  30083  trlreslem  30084  upgrwlkdvdelem  30122  pthdlem1  30152  pthdlem2lem  30153  uspgrn2crct  30194  wlkiswwlks2lem3  30257  wlkiswwlksupgr2  30263  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  1wlkdlem1  30525  wlk2v2e  30545  eucrctshift  30631  konigsbergssiedgw  30638  wrdres  33292  pfxf1  33299  s3f1  33301  cycpmcl  33467  tocyc01  33469  cycpmco2rn  33476  cycpmrn  33494  tocyccntz  33495  cycpmconjslem2  33506  unitprodclb  33733  sseqf  34814  fiblem  34820  ofcccat  34965  signstcl  34984  signstf  34985  signstfvn  34988  signsvtn0  34989  signstres  34994  signsvtp  35002  signsvtn  35003  signsvfpn  35004  signsvfnn  35005  signshf  35007  revwlk  35638  mvrsfpw  36019  frlmfzowrdb  43319  amgm2d  44965  amgm3d  44966  amgm4d  44967  chnsubseqword  47635  chnsubseqwl  47636  chnsubseq  47637  lswn0  48234  upgrimwlklem1  48703  upgrimwlklem2  48704  upgrimwlklem3  48705  upgrimtrlslem1  48710  upgrimtrlslem2  48711  gpgprismgr4cycllem9  48909  wrdf1d  50663  amgmw2d  50693