This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi 
 |-  ( 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 biimtrdi 
 |-  ( -. L e. ZZ -> ( W : ( 0 ... L ) --> S -> W e. Word S ) )
13 4 12 pm2.61i 
 |-  ( W : ( 0 ... L ) --> S -> W e. Word S )