Metamath Proof Explorer


Theorem iswrdb

Description: A word over an alphabet is a function from an open range of nonnegative integers (of length equal to the length of the word) into the alphabet. (Contributed by Alexander van der Vekens, 30-Jul-2018)

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

Proof

Step Hyp Ref Expression
1 wrdf
 |-  ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S )
2 iswrdi
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> S -> W e. Word S )
3 1 2 impbii
 |-  ( W e. Word S <-> W : ( 0 ..^ ( # ` W ) ) --> S )