Theorem wrdf 14528

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 14525	. 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆)
2		simpr 488	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆)
3		fnfzo0hash 14460	. . . . . 6 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙)
4	3	oveq2d 7408	. . . . 5 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙))
5	4	feq2d 6671	. . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0..^𝑙)⟶𝑆))
6	2, 5	mpbird 259	. . 3 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
7	6	rexlimiva 3154	. 2 ⊢ (∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
8	1, 7	sylbi 219	1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085  ⟶wf 6513  ‘cfv 6517  (class class class)co 7392  0cc0 11070  ℕ₀cn0 12478  ..^cfzo 13656  ♯chash 14340  Word cword 14523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-cnex 11126  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4905  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-om 7843  df-1st 7966  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-1o 8432  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-fin 8927  df-card 9894  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-nn 12208  df-n0 12479  df-z 12566  df-uz 12837  df-fz 13510  df-fzo 13657  df-hash 14341  df-word 14524

This theorem is referenced by:  wrdfd  14529  iswrdb  14530  wrddm  14531  wrdsymbcl  14537  wrdfn  14538  wrdffz  14545  0wrd0  14550  wrdsymb  14552  wrdnval  14555  wrdred1  14570  wrdred1hash  14571  ccatcl  14584  ccatalpha  14604  s1dm  14619  swrdcl  14656  swrdf  14661  swrdwrdsymb  14673  pfxres  14690  cats1un  14731  revcl  14771  revlen  14772  revrev  14777  repsdf2  14788  cshwf  14810  cshinj  14821  wrdco  14841  lenco  14842  revco  14844  ccatco  14845  lswco  14849  s2dm  14900  wwlktovf  14966  s7f1o  14976  ofccat  14979  chnf  18644  gsumwsubmcl  18854  gsumsgrpccat  18857  gsumwmhm  18862  frmdss2  18880  symgtrinv  19495  psgnunilem5  19517  psgnunilem2  19518  psgnunilem3  19519  efginvrel1  19751  efgsf  19752  efgsrel  19757  efgs1b  19759  efgredlemf  19764  efgredlemd  19767  efgredlemc  19768  efgredlem  19770  frgpup3lem  19800  pgpfaclem1  20106  ablfaclem2  20111  ablfaclem3  20112  ablfac2  20114  dchrptlem1  27305  dchrptlem2  27306  trgcgrg  28661  tgcgr4  28677  wrdupgr  29232  wrdumgr  29244  vdegp1ai  29683  vdegp1bi  29684  wlkres  29815  wlkp1  29826  wlkdlem1  29827  trlf1  29843  trlreslem  29844  upgrwlkdvdelem  29882  pthdlem1  29912  pthdlem2lem  29913  uspgrn2crct  29954  wlkiswwlks2lem3  30017  wlkiswwlksupgr2  30023  clwlkclwwlklem2a  30146  clwlkclwwlklem2  30148  1wlkdlem1  30285  wlk2v2e  30305  eucrctshift  30391  konigsbergssiedgw  30398  wrdres  33074  pfxf1  33081  s3f1  33086  ccatf1  33088  swrdrn3  33094  cycpmcl  33257  tocyc01  33259  cycpmco2rn  33266  cycpmrn  33284  tocyccntz  33285  cycpmconjslem2  33296  unitprodclb  33536  sseqf  34650  fiblem  34656  ofcccat  34801  signstcl  34823  signstf  34824  signstfvn  34827  signsvtn0  34828  signstres  34833  signsvtp  34841  signsvtn  34842  signsvfpn  34843  signsvfnn  34844  signshf  34846  revwlk  35439  mvrsfpw  35820  frlmfzowrdb  43090  amgm2d  44738  amgm3d  44739  amgm4d  44740  chnsubseqword  47418  chnsubseqwl  47419  chnsubseq  47420  lswn0  48014  upgrimwlklem1  48483  upgrimwlklem2  48484  upgrimwlklem3  48485  upgrimtrlslem1  48490  upgrimtrlslem2  48491  gpgprismgr4cycllem9  48689  amgmw2d  50389