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

Metamath Proof Explorer

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 )