Metamath Proof Explorer


Theorem wrdfd

Description: A word is a zero-based sequence with a recoverable upper limit, deduction version. (Contributed by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Hypotheses wrdfd.n
|- ( ph -> N = ( # ` W ) )
wrdfd.w
|- ( ph -> W e. Word S )
Assertion wrdfd
|- ( ph -> W : ( 0 ..^ N ) --> S )

Proof

Step Hyp Ref Expression
1 wrdfd.n
 |-  ( ph -> N = ( # ` W ) )
2 wrdfd.w
 |-  ( ph -> W e. Word S )
3 wrdf
 |-  ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S )
4 2 3 syl
 |-  ( ph -> W : ( 0 ..^ ( # ` W ) ) --> S )
5 1 oveq2d
 |-  ( ph -> ( 0 ..^ N ) = ( 0 ..^ ( # ` W ) ) )
6 5 feq2d
 |-  ( ph -> ( W : ( 0 ..^ N ) --> S <-> W : ( 0 ..^ ( # ` W ) ) --> S ) )
7 4 6 mpbird
 |-  ( ph -> W : ( 0 ..^ N ) --> S )