Metamath Proof Explorer


Theorem swrdvalfn

Description: Value of the subword extractor as function with domain. (Contributed by Alexander van der Vekens, 28-Mar-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion swrdvalfn ( ( 𝑆 ∈ Word 𝑉𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) Fn ( 0 ..^ ( 𝐿𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 swrdf ( ( 𝑆 ∈ Word 𝑉𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) : ( 0 ..^ ( 𝐿𝐹 ) ) ⟶ 𝑉 )
2 1 ffnd ( ( 𝑆 ∈ Word 𝑉𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) Fn ( 0 ..^ ( 𝐿𝐹 ) ) )