Theorem wrdf 14643

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3087  ⟶wf 6527  ‘cfv 6531  (class class class)co 7412  0cc0 11181  ℕ₀cn0 12587  ..^cfzo 13768  ♯chash 14454  Word cword 14638

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-card 10001  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-nn 12317  df-n0 12588  df-z 12675  df-uz 12947  df-fz 13621  df-fzo 13769  df-hash 14455  df-word 14639

This theorem is used by:  wrdfd  14644  iswrdb  14645  wrddm  14646  wrdsymbcl  14652  wrdfn  14653  wrdffz  14660  0wrd0  14665  wrdsymb  14667  wrdnval  14670  wrdred1  14685  wrdred1hash  14686  ccatcl  14699  ccatf1  14716  ccatalpha  14720  s1dm  14735  swrdcl  14773  swrdf  14778  swrdrn3  14782  swrdwrdsymb  14792  pfxres  14809  cats1un  14850  revcl  14890  revlen  14891  revrev  14896  repsdf2  14909  cshwf  14931  cshinj  14942  wrdco  14962  lenco  14963  revco  14965  ccatco  14966  lswco  14970  s2dm  15021  wwlktovf  15089  s7f1o  15099  ofccat  15102  chnf  18783  gsumwsubmcl  19013  gsumsgrpccat  19016  gsumwmhm  19021  frmdss2  19039  symgtrinv  19666  psgnunilem5  19688  psgnunilem2  19689  psgnunilem3  19690  efginvrel1  19922  efgsf  19923  efgsrel  19928  efgs1b  19930  efgredlemf  19935  efgredlemd  19938  efgredlemc  19939  efgredlem  19941  frgpup3lem  19971  pgpfaclem1  20277  ablfaclem2  20282  ablfaclem3  20283  ablfac2  20285  dchrptlem1  27573  dchrptlem2  27574  trgcgrg  28960  tgcgr4  28976  wrdupgr  29645  wrdumgr  29657  vdegp1ai  30099  vdegp1bi  30100  wlkres  30231  wlkp1  30242  wlkdlem1  30243  revwlk  30249  trlf1  30263  trlreslem  30264  upgrwlkdvdelem  30304  pthdlem1  30334  pthdlem2lem  30335  uspgrn2crct  30379  wlkiswwlks2lem3  30442  wlkiswwlksupgr2  30448  clwlkclwwlklem2a  30571  clwlkclwwlklem2  30573  1wlkdlem1  30710  wlk2v2e  30740  eucrctshift  30826  konigsbergssiedgw  30833  wrdres  33484  pfxf1  33491  s3f1  33493  cycpmcl  33659  tocyc01  33661  cycpmco2rn  33668  cycpmrn  33686  tocyccntz  33687  cycpmconjslem2  33698  unitprodclb  33926  sseqf  35007  fiblem  35013  ofcccat  35158  signstcl  35177  signstf  35178  signstfvn  35181  signsvtn0  35182  signstres  35187  signsvtp  35195  signsvtn  35196  signsvfpn  35197  signsvfnn  35198  signshf  35200  mvrsfpw  36240  frlmfzowrdb  43536  amgm2d  45157  amgm3d  45158  amgm4d  45159  chnsubseqword  47832  chnsubseqwl  47833  chnsubseq  47834  wrddin  47840  lswn0  48470  upgrimwlklem1  48939  upgrimwlklem2  48940  upgrimwlklem3  48941  upgrimtrlslem1  48946  upgrimtrlslem2  48947  gpgprismgr4cycllem9  49145  wrdf1d  50884  amgmw2d  50933