Theorem ffz0iswrd

Description: A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018) (Proof shortened by AV, 13-Oct-2018) (Proof shortened by JJ, 18-Nov-2022)

	Ref	Expression
Assertion	ffz0iswrd	|- ( W : ( 0 ... L ) --> S -> W e. Word S )

Proof

Step	Hyp	Ref	Expression
1		fzval3	|- ( L e. ZZ -> ( 0 ... L ) = ( 0 ..^ ( L + 1 ) ) )
2	1	feq2d	|- ( L e. ZZ -> ( W : ( 0 ... L ) --> S <-> W : ( 0 ..^ ( L + 1 ) ) --> S ) )
3		iswrdi	|- ( W : ( 0 ..^ ( L + 1 ) ) --> S -> W e. Word S )
4	2 3	syl6bi	|- ( L e. ZZ -> ( W : ( 0 ... L ) --> S -> W e. Word S ) )
5		fzn0	|- ( ( 0 ... L ) =/= (/) <-> L e. ( ZZ>= ` 0 ) )
6		elnn0uz	|- ( L e. NN0 <-> L e. ( ZZ>= ` 0 ) )
7	5 6	sylbb2	|- ( ( 0 ... L ) =/= (/) -> L e. NN0 )
8	7	nn0zd	|- ( ( 0 ... L ) =/= (/) -> L e. ZZ )
9	8	necon1bi	|- ( -. L e. ZZ -> ( 0 ... L ) = (/) )
10	9	feq2d	|- ( -. L e. ZZ -> ( W : ( 0 ... L ) --> S <-> W : (/) --> S ) )
11		iswrddm0	|- ( W : (/) --> S -> W e. Word S )
12	10 11	syl6bi	|- ( -. L e. ZZ -> ( W : ( 0 ... L ) --> S -> W e. Word S ) )
13	4 12	pm2.61i	|- ( W : ( 0 ... L ) --> S -> W e. Word S )