| 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 14521 | . 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆) | |
| 2 | simpr 488 | . . . 4 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆) | |
| 3 | fnfzo0hash 14456 | . . . . . 6 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙) | |
| 4 | 3 | oveq2d 7406 | . . . . 5 ⊢ ((𝑙 ∈ ℕ0 ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙)) |
| 5 | 4 | feq2d 6669 | . . . 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..^(♯‘𝑊))⟶𝑆) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2141 ∃wrex 3085 ⟶wf 6511 ‘cfv 6515 (class class class)co 7390 0cc0 11066 ℕ0cn0 12474 ..^cfzo 13652 ♯chash 14336 Word cword 14519 |
| 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 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143 |
| 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 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-er 8671 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-card 9890 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-nn 12204 df-n0 12475 df-z 12562 df-uz 12833 df-fz 13506 df-fzo 13653 df-hash 14337 df-word 14520 |
| This theorem is referenced by: wrdfd 14525 iswrdb 14526 wrddm 14527 wrdsymbcl 14533 wrdfn 14534 wrdffz 14541 0wrd0 14546 wrdsymb 14548 wrdnval 14551 wrdred1 14566 wrdred1hash 14567 ccatcl 14580 ccatalpha 14600 s1dm 14615 swrdcl 14652 swrdf 14657 swrdwrdsymb 14669 pfxres 14686 cats1un 14727 revcl 14767 revlen 14768 revrev 14773 repsdf2 14784 cshwf 14806 cshinj 14817 wrdco 14837 lenco 14838 revco 14840 ccatco 14841 lswco 14845 s2dm 14896 wwlktovf 14962 s7f1o 14972 ofccat 14975 chnf 18651 gsumwsubmcl 18861 gsumsgrpccat 18864 gsumwmhm 18869 frmdss2 18887 symgtrinv 19502 psgnunilem5 19524 psgnunilem2 19525 psgnunilem3 19526 efginvrel1 19758 efgsf 19759 efgsrel 19764 efgs1b 19766 efgredlemf 19771 efgredlemd 19774 efgredlemc 19775 efgredlem 19777 frgpup3lem 19807 pgpfaclem1 20113 ablfaclem2 20118 ablfaclem3 20119 ablfac2 20121 dchrptlem1 27315 dchrptlem2 27316 trgcgrg 28671 tgcgr4 28687 wrdupgr 29242 wrdumgr 29254 vdegp1ai 29693 vdegp1bi 29694 wlkres 29825 wlkp1 29836 wlkdlem1 29837 trlf1 29853 trlreslem 29854 upgrwlkdvdelem 29892 pthdlem1 29922 pthdlem2lem 29923 uspgrn2crct 29964 wlkiswwlks2lem3 30027 wlkiswwlksupgr2 30033 clwlkclwwlklem2a 30156 clwlkclwwlklem2 30158 1wlkdlem1 30295 wlk2v2e 30315 eucrctshift 30401 konigsbergssiedgw 30408 wrdres 33073 pfxf1 33080 s3f1 33085 ccatf1 33087 swrdrn3 33093 cycpmcl 33256 tocyc01 33258 cycpmco2rn 33265 cycpmrn 33283 tocyccntz 33284 cycpmconjslem2 33295 unitprodclb 33535 sseqf 34649 fiblem 34655 ofcccat 34800 signstcl 34819 signstf 34820 signstfvn 34823 signsvtn0 34824 signstres 34829 signsvtp 34837 signsvtn 34838 signsvfpn 34839 signsvfnn 34840 signshf 34842 revwlk 35435 mvrsfpw 35816 frlmfzowrdb 43086 amgm2d 44734 amgm3d 44735 amgm4d 44736 chnsubseqword 47414 chnsubseqwl 47415 chnsubseq 47416 lswn0 48010 upgrimwlklem1 48479 upgrimwlklem2 48480 upgrimwlklem3 48481 upgrimtrlslem1 48486 upgrimtrlslem2 48487 gpgprismgr4cycllem9 48685 amgmw2d 50385 |
| Copyright terms: Public domain | W3C validator |