Theorem wrdfn 14266

Description: A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018.)

Assertion

Ref	Expression
wrdfn	⊢ (𝑊 ∈ Word 𝑆 → 𝑊 Fn (0..^(♯‘𝑊)))

Proof of Theorem wrdfn

Step	Hyp	Ref	Expression
1		wrdf 14257	. 2 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
2	1	ffnd 6626	1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊 Fn (0..^(♯‘𝑊)))

Syntax hints:   → wi 4   ∈ wcel 2102   Fn wfn 6448  ‘cfv 6453  (class class class)co 7302  0cc0 10906  ..^cfzo 13417  ♯chash 14079  Word cword 14252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2104  ax-9 2112  ax-10 2133  ax-11 2150  ax-12 2167  ax-ext 2705  ax-rep 5216  ax-sep 5230  ax-nul 5237  ax-pow 5295  ax-pr 5359  ax-un 7615  ax-cnex 10962  ax-resscn 10963  ax-1cn 10964  ax-icn 10965  ax-addcl 10966  ax-addrcl 10967  ax-mulcl 10968  ax-mulrcl 10969  ax-mulcom 10970  ax-addass 10971  ax-mulass 10972  ax-distr 10973  ax-i2m1 10974  ax-1ne0 10975  ax-1rid 10976  ax-rnegex 10977  ax-rrecex 10978  ax-cnre 10979  ax-pre-lttri 10980  ax-pre-lttrn 10981  ax-pre-ltadd 10982  ax-pre-mulgt0 10983

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2536  df-eu 2565  df-clab 2712  df-cleq 2726  df-clel 2812  df-nfc 2885  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3224  df-rab 3225  df-v 3437  df-sbc 3720  df-csb 3836  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3909  df-nul 4261  df-if 4464  df-pw 4539  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4843  df-int 4885  df-iun 4931  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5495  df-eprel 5501  df-po 5509  df-so 5510  df-fr 5550  df-we 5552  df-xp 5601  df-rel 5602  df-cnv 5603  df-co 5604  df-dm 5605  df-rn 5606  df-res 5607  df-ima 5608  df-pred 6212  df-ord 6279  df-on 6280  df-lim 6281  df-suc 6282  df-iota 6405  df-fun 6455  df-fn 6456  df-f 6457  df-f1 6458  df-fo 6459  df-f1o 6460  df-fv 6461  df-riota 7259  df-ov 7305  df-oprab 7306  df-mpo 7307  df-om 7740  df-1st 7858  df-2nd 7859  df-frecs 8124  df-wrecs 8155  df-recs 8229  df-rdg 8268  df-1o 8324  df-er 8525  df-en 8761  df-dom 8762  df-sdom 8763  df-fin 8764  df-card 9732  df-pnf 11046  df-mnf 11047  df-xr 11048  df-ltxr 11049  df-le 11050  df-sub 11242  df-neg 11243  df-nn 12009  df-n0 12269  df-z 12355  df-uz 12618  df-fz 13275  df-fzo 13418  df-hash 14080  df-word 14253

This theorem is referenced by:  iswrdsymb  14269  wrdfin  14270  eqwrd  14295  ccatlid  14326  ccatrid  14327  ccatass  14328  ccatrn  14329  ccatswrd  14416  swrdccat2  14417  pfxid  14432  ccatpfx  14449  pfxccat1  14450  revccat  14514  revrev  14515  cshimadifsn  14577  revco  14582  cshco  14584  swrdco  14585  s3fn  14659  wrd2pr2op  14691  wrd3tpop  14696  pgpfaclem1  19719  wlkp1lem2  28077  wwlksm1edg  28281  s2rn  31253  s3rn  31255  cshwrnid  31268  cycpmfvlem  31414  cycpmfv1  31415  cycpmfv2  31416  cycpmfv3  31417  cycpmconjslem1  31456  cycpmconjslem2  31457  sseqfv1  32391  sseqfn  32392  sseqfres  32395  sseqfv2  32396  signstres  32589  revpfxsfxrev  33112