Theorem wrdf

Description: A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015)

	Ref	Expression
Assertion	wrdf	|- ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S )

Proof

Step	Hyp	Ref	Expression
1		iswrd	|- ( W e. Word S <-> E. l e. NN0 W : ( 0 ..^ l ) --> S )
2		simpr	|- ( ( l e. NN0 /\ W : ( 0 ..^ l ) --> S ) -> W : ( 0 ..^ l ) --> S )
3		fnfzo0hash	|- ( ( l e. NN0 /\ W : ( 0 ..^ l ) --> S ) -> ( # ` W ) = l )
4	3	oveq2d	|- ( ( l e. NN0 /\ W : ( 0 ..^ l ) --> S ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ l ) )
5	4	feq2d	|- ( ( l e. NN0 /\ W : ( 0 ..^ l ) --> S ) -> ( W : ( 0 ..^ ( # ` W ) ) --> S <-> W : ( 0 ..^ l ) --> S ) )
6	2 5	mpbird	|- ( ( l e. NN0 /\ W : ( 0 ..^ l ) --> S ) -> W : ( 0 ..^ ( # ` W ) ) --> S )
7	6	rexlimiva	|- ( E. l e. NN0 W : ( 0 ..^ l ) --> S -> W : ( 0 ..^ ( # ` W ) ) --> S )
8	1 7	sylbi	|- ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S )