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 )