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\leftrightarrow \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$
2		simpr	$$⊢\left(l\in {\mathbb{N}}_0\wedge W:\left(0..^l\right)⟶S\right)\to W:\left(0..^l\right)⟶S$$
3		fnfzo0hash	$$⊢\left(l\in {\mathbb{N}}_0\wedge W:\left(0..^l\right)⟶S\right)\to \left|W\right|=l$$
4	3	oveq2d	$$⊢\left(l\in {\mathbb{N}}_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 {\mathbb{N}}_0\wedge W:\left(0..^l\right)⟶S\right)\to \left(W:\left(0..^\left|W\right|\right)⟶S\leftrightarrow W:\left(0..^l\right)⟶S\right)$$
6	2 5	mpbird	$$⊢\left(l\in {\mathbb{N}}_0\wedge W:\left(0..^l\right)⟶S\right)\to W:\left(0..^\left|W\right|\right)⟶S$$
7	6	rexlimiva	$$⊢\exists l\in {\mathbb{N}}_{0}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$$