wrdf - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wrdf		Structured version Visualization version GIF version

Theorem wrdf 14150

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 14147	. 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆)
2		simpr 484	. . . 4 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆)
3		fnfzo0hash 14090	. . . . . 6 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙)
4	3	oveq2d 7271	. . . . 5 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙))
5	4	feq2d 6570	. . . 4 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0..^𝑙)⟶𝑆))
6	2, 5	mpbird 256	. . 3 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
7	6	rexlimiva 3209	. 2 ⊢ (∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
8	1, 7	sylbi 216	1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∃wrex 3064 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 0cc0 10802 ℕ₀cn0 12163 ..^cfzo 13311 ♯chash 13972 Word cword 14145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169 df-fzo 13312 df-hash 13973 df-word 14146

This theorem is referenced by: iswrdb 14151 wrddm 14152 wrdsymbcl 14158 wrdfn 14159 wrdffz 14166 0wrd0 14171 wrdsymb 14173 wrdnval 14176 wrdred1 14191 wrdred1hash 14192 ccatcl 14205 ccatalpha 14226 s1dm 14241 swrdcl 14286 swrdf 14291 swrdwrdsymb 14303 pfxres 14320 cats1un 14362 revcl 14402 revlen 14403 revrev 14408 repsdf2 14419 cshwf 14441 cshinj 14452 wrdco 14472 lenco 14473 revco 14475 ccatco 14476 lswco 14480 s2dm 14531 wwlktovf 14599 ofccat 14608 gsumwsubmcl 18390 gsumsgrpccat 18393 gsumccatOLD 18394 gsumwmhm 18399 frmdss2 18417 symgtrinv 18995 psgnunilem5 19017 psgnunilem2 19018 psgnunilem3 19019 efginvrel1 19249 efgsf 19250 efgsrel 19255 efgs1b 19257 efgredlemf 19262 efgredlemd 19265 efgredlemc 19266 efgredlem 19268 frgpup3lem 19298 pgpfaclem1 19599 ablfaclem2 19604 ablfaclem3 19605 ablfac2 19607 dchrptlem1 26317 dchrptlem2 26318 trgcgrg 26780 tgcgr4 26796 wrdupgr 27358 wrdumgr 27370 vdegp1ai 27806 vdegp1bi 27807 wlkres 27940 wlkp1 27951 wlkdlem1 27952 trlf1 27968 trlreslem 27969 upgrwlkdvdelem 28005 pthdlem1 28035 pthdlem2lem 28036 uspgrn2crct 28074 wlkiswwlks2lem3 28137 wlkiswwlksupgr2 28143 clwlkclwwlklem2a 28263 clwlkclwwlklem2 28265 1wlkdlem1 28402 wlk2v2e 28422 eucrctshift 28508 konigsbergssiedgw 28515 wrdfd 31112 wrdres 31113 pfxf1 31118 s3f1 31123 ccatf1 31125 swrdrn3 31129 cycpmcl 31285 tocyc01 31287 cycpmco2rn 31294 cycpmrn 31312 tocyccntz 31313 cycpmconjslem2 31324 sseqf 32259 fiblem 32265 ofcccat 32422 signstcl 32444 signstf 32445 signstfvn 32448 signsvtn0 32449 signstres 32454 signsvtp 32462 signsvtn 32463 signsvfpn 32464 signsvfnn 32465 signshf 32467 revwlk 32986 mvrsfpw 33368 frlmfzowrdb 40161 amgm2d 41698 amgm3d 41699 amgm4d 41700 lswn0 44784 amgmw2d 46394

W3C validator