![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > wrdf | Structured version Visualization version GIF version |
Description: A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
Ref | Expression |
---|---|
wrdf | ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iswrd 13577 | . 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆) | |
2 | simpr 479 | . . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆) | |
3 | fnfzo0hash 13524 | . . . . . 6 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙) | |
4 | 3 | oveq2d 6922 | . . . . 5 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙)) |
5 | 4 | feq2d 6265 | . . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0..^𝑙)⟶𝑆)) |
6 | 2, 5 | mpbird 249 | . . 3 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^(♯‘𝑊))⟶𝑆) |
7 | 6 | rexlimiva 3238 | . 2 ⊢ (∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆) |
8 | 1, 7 | sylbi 209 | 1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2166 ∃wrex 3119 ⟶wf 6120 ‘cfv 6124 (class class class)co 6906 0cc0 10253 ℕ0cn0 11619 ..^cfzo 12761 ♯chash 13411 Word cword 13575 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-rep 4995 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 ax-cnex 10309 ax-resscn 10310 ax-1cn 10311 ax-icn 10312 ax-addcl 10313 ax-addrcl 10314 ax-mulcl 10315 ax-mulrcl 10316 ax-mulcom 10317 ax-addass 10318 ax-mulass 10319 ax-distr 10320 ax-i2m1 10321 ax-1ne0 10322 ax-1rid 10323 ax-rnegex 10324 ax-rrecex 10325 ax-cnre 10326 ax-pre-lttri 10327 ax-pre-lttrn 10328 ax-pre-ltadd 10329 ax-pre-mulgt0 10330 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-nel 3104 df-ral 3123 df-rex 3124 df-reu 3125 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-pss 3815 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4660 df-int 4699 df-iun 4743 df-br 4875 df-opab 4937 df-mpt 4954 df-tr 4977 df-id 5251 df-eprel 5256 df-po 5264 df-so 5265 df-fr 5302 df-we 5304 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-pred 5921 df-ord 5967 df-on 5968 df-lim 5969 df-suc 5970 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-riota 6867 df-ov 6909 df-oprab 6910 df-mpt2 6911 df-om 7328 df-1st 7429 df-2nd 7430 df-wrecs 7673 df-recs 7735 df-rdg 7773 df-1o 7827 df-er 8010 df-en 8224 df-dom 8225 df-sdom 8226 df-fin 8227 df-card 9079 df-pnf 10394 df-mnf 10395 df-xr 10396 df-ltxr 10397 df-le 10398 df-sub 10588 df-neg 10589 df-nn 11352 df-n0 11620 df-z 11706 df-uz 11970 df-fz 12621 df-fzo 12762 df-hash 13412 df-word 13576 |
This theorem is referenced by: iswrdb 13581 wrddm 13582 wrdsymbcl 13588 wrdfn 13589 wrdv 13590 wrdffz 13596 0wrd0 13601 wrdsymb 13603 wrdnval 13606 wrdred1 13621 wrdred1hash 13622 ccatcl 13635 ccatass 13649 ccatrn 13650 ccatalpha 13654 s1dm 13669 swrdcl 13706 swrd0valOLD 13708 swrdf 13713 swrdnd2 13721 swrdwrdsymb 13737 ccatswrd 13747 swrdccat1OLD 13748 swrdccat2 13749 pfxres 13759 ccatpfx 13781 cats1un 13812 revcl 13878 revlen 13879 revccat 13883 revrev 13884 repsdf2 13895 cshwf 13922 cshinj 13933 wrdco 13953 lenco 13954 revco 13956 ccatco 13957 lswco 13961 s2dm 14012 wwlktovf 14079 ofccat 14088 gsumwsubmcl 17729 gsumccat 17732 gsumwmhm 17737 frmdss2 17755 symgtrinv 18243 psgnunilem5 18265 psgnunilem5OLD 18266 psgnunilem2 18267 psgnunilem3 18268 efginvrel1 18493 efgsf 18494 efgsrel 18499 efgs1b 18501 efgredlemf 18507 efgredlemd 18510 efgredlemc 18511 efgredlem 18513 efgredlemOLD 18514 frgpup3lem 18544 pgpfaclem1 18835 ablfaclem2 18840 ablfaclem3 18841 ablfac2 18843 dchrptlem1 25403 dchrptlem2 25404 trgcgrg 25828 tgcgr4 25844 wrdupgr 26384 wrdumgr 26396 vdegp1ai 26835 vdegp1bi 26836 wlkres 26970 wlkreslemOLD 26971 wlkresOLD 26972 wlkp1 26983 wlkdlem1 26984 trlf1 27000 trlreslem 27001 trlreslemOLD 27003 upgrwlkdvdelem 27039 pthdlem1 27069 pthdlem2lem 27070 uspgrn2crct 27108 wlkiswwlks2lem3 27171 wlkiswwlksupgr2 27177 clwlkclwwlklem2a 27328 clwlkclwwlklem2 27330 1wlkdlem1 27514 wlk2v2e 27534 eucrctshift 27621 konigsbergssiedgw 27630 sseqf 31001 fiblem 31007 wrdfd 31163 wrdres 31164 ofcccat 31168 signstcl 31190 signstf 31191 signstfvn 31194 signsvtn0 31195 signsvtn0OLD 31196 signstres 31201 signsvtp 31210 signsvtn 31211 signsvfpn 31212 signsvfnn 31213 signshf 31215 mvrsfpw 31950 amgm2d 39342 amgm3d 39343 amgm4d 39344 lswn0 42269 amgmw2d 43447 |
Copyright terms: Public domain | W3C validator |