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 )