Theorem iswrdi

Description: A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢l=L\to \left(0..^l\right)=\left(0..^L\right)$$
2	1	feq2d	$$⊢l=L\to \left(W:\left(0..^l\right)⟶S\leftrightarrow W:\left(0..^L\right)⟶S\right)$$
3	2	rspcev	$$⊢\left(L\in {\mathbb{N}}_0\wedge W:\left(0..^L\right)⟶S\right)\to \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5		fzo0n0	$$⊢\left(0..^L\right)\ne \varnothing \leftrightarrow L\in \mathbb{N}$$
6		nnnn0	$$⊢L\in \mathbb{N}\to L\in {\mathbb{N}}_0$$
7	5 6	sylbi	$$⊢\left(0..^L\right)\ne \varnothing \to L\in {\mathbb{N}}_0$$
8	7	necon1bi	$$⊢\neg L\in {\mathbb{N}}_0\to \left(0..^L\right)=\varnothing$$
9		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
10	8 9	syl6eqr	$$⊢\neg L\in {\mathbb{N}}_0\to \left(0..^L\right)=\left(0..^0\right)$$
11	10	feq2d	$$⊢\neg L\in {\mathbb{N}}_0\to \left(W:\left(0..^L\right)⟶S\leftrightarrow W:\left(0..^0\right)⟶S\right)$$
12	11	biimpa	$$⊢\left(\neg L\in {\mathbb{N}}_0\wedge W:\left(0..^L\right)⟶S\right)\to W:\left(0..^0\right)⟶S$$
13		oveq2	$$⊢l=0\to \left(0..^l\right)=\left(0..^0\right)$$
14	13	feq2d	$$⊢l=0\to \left(W:\left(0..^l\right)⟶S\leftrightarrow W:\left(0..^0\right)⟶S\right)$$
15	14	rspcev	$$⊢\left(0\in {\mathbb{N}}_0\wedge W:\left(0..^0\right)⟶S\right)\to \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$
16	4 12 15	sylancr	$$⊢\left(\neg L\in {\mathbb{N}}_0\wedge W:\left(0..^L\right)⟶S\right)\to \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$
17	3 16	pm2.61ian	$$⊢W:\left(0..^L\right)⟶S\to \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$
18		iswrd	$$⊢W\in \mathrm{Word}S\leftrightarrow \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$
19	17 18	sylibr	$$⊢W:\left(0..^L\right)⟶S\to W\in \mathrm{Word}S$$