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 ( 𝜑𝑁 = ( ♯ ‘ 𝑊 ) )
wrdfd.w ( 𝜑𝑊 ∈ Word 𝑆 )
Assertion wrdfd ( 𝜑𝑊 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )

Proof

Step Hyp Ref Expression
1 wrdfd.n ( 𝜑𝑁 = ( ♯ ‘ 𝑊 ) )
2 wrdfd.w ( 𝜑𝑊 ∈ Word 𝑆 )
3 wrdf ( 𝑊 ∈ Word 𝑆𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
4 2 3 syl ( 𝜑𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
5 1 oveq2d ( 𝜑 → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 5 feq2d ( 𝜑 → ( 𝑊 : ( 0 ..^ 𝑁 ) ⟶ 𝑆𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 ) )
7 4 6 mpbird ( 𝜑𝑊 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )