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

Metamath Proof Explorer

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 : ( 0 ..^ L ) --> S -> W e. Word S )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( l = L -> ( 0 ..^ l ) = ( 0 ..^ L ) )
2 1 feq2d 
 |-  ( l = L -> ( W : ( 0 ..^ l ) --> S <-> W : ( 0 ..^ L ) --> S ) )
3 2 rspcev 
 |-  ( ( L e. NN0 /\ W : ( 0 ..^ L ) --> S ) -> E. l e. NN0 W : ( 0 ..^ l ) --> S )
4 0nn0 
 |-  0 e. NN0
5 fzo0n0 
 |-  ( ( 0 ..^ L ) =/= (/) <-> L e. NN )
6 nnnn0 
 |-  ( L e. NN -> L e. NN0 )
7 5 6 sylbi 
 |-  ( ( 0 ..^ L ) =/= (/) -> L e. NN0 )
8 7 necon1bi 
 |-  ( -. L e. NN0 -> ( 0 ..^ L ) = (/) )
9 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
10 8 9 eqtr4di 
 |-  ( -. L e. NN0 -> ( 0 ..^ L ) = ( 0 ..^ 0 ) )
11 10 feq2d 
 |-  ( -. L e. NN0 -> ( W : ( 0 ..^ L ) --> S <-> W : ( 0 ..^ 0 ) --> S ) )
12 11 biimpa 
 |-  ( ( -. L e. NN0 /\ W : ( 0 ..^ L ) --> S ) -> W : ( 0 ..^ 0 ) --> S )
13 oveq2 
 |-  ( l = 0 -> ( 0 ..^ l ) = ( 0 ..^ 0 ) )
14 13 feq2d 
 |-  ( l = 0 -> ( W : ( 0 ..^ l ) --> S <-> W : ( 0 ..^ 0 ) --> S ) )
15 14 rspcev 
 |-  ( ( 0 e. NN0 /\ W : ( 0 ..^ 0 ) --> S ) -> E. l e. NN0 W : ( 0 ..^ l ) --> S )
16 4 12 15 sylancr 
 |-  ( ( -. L e. NN0 /\ W : ( 0 ..^ L ) --> S ) -> E. l e. NN0 W : ( 0 ..^ l ) --> S )
17 3 16 pm2.61ian 
 |-  ( W : ( 0 ..^ L ) --> S -> E. l e. NN0 W : ( 0 ..^ l ) --> S )
18 iswrd 
 |-  ( W e. Word S <-> E. l e. NN0 W : ( 0 ..^ l ) --> S )
19 17 18 sylibr 
 |-  ( W : ( 0 ..^ L ) --> S -> W e. Word S )