# Metamath Proof Explorer

## Theorem wrdf

Description: A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion wrdf ${⊢}{W}\in \mathrm{Word}{S}\to {W}:\left(0..^\left|{W}\right|\right)⟶{S}$

### Proof

Step Hyp Ref Expression
1 iswrd ${⊢}{W}\in \mathrm{Word}{S}↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{S}$
2 simpr ${⊢}\left({l}\in {ℕ}_{0}\wedge {W}:\left(0..^{l}\right)⟶{S}\right)\to {W}:\left(0..^{l}\right)⟶{S}$
3 fnfzo0hash ${⊢}\left({l}\in {ℕ}_{0}\wedge {W}:\left(0..^{l}\right)⟶{S}\right)\to \left|{W}\right|={l}$
4 3 oveq2d ${⊢}\left({l}\in {ℕ}_{0}\wedge {W}:\left(0..^{l}\right)⟶{S}\right)\to \left(0..^\left|{W}\right|\right)=\left(0..^{l}\right)$
5 4 feq2d ${⊢}\left({l}\in {ℕ}_{0}\wedge {W}:\left(0..^{l}\right)⟶{S}\right)\to \left({W}:\left(0..^\left|{W}\right|\right)⟶{S}↔{W}:\left(0..^{l}\right)⟶{S}\right)$
6 2 5 mpbird ${⊢}\left({l}\in {ℕ}_{0}\wedge {W}:\left(0..^{l}\right)⟶{S}\right)\to {W}:\left(0..^\left|{W}\right|\right)⟶{S}$
7 6 rexlimiva ${⊢}\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{S}\to {W}:\left(0..^\left|{W}\right|\right)⟶{S}$
8 1 7 sylbi ${⊢}{W}\in \mathrm{Word}{S}\to {W}:\left(0..^\left|{W}\right|\right)⟶{S}$