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 ( 𝑊 ∈ Word 𝑆𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )

Proof

Step Hyp Ref Expression
1 wrdf ( 𝑊 ∈ Word 𝑆𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
2 iswrdi ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆𝑊 ∈ Word 𝑆 )
3 1 2 impbii ( 𝑊 ∈ Word 𝑆𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )