Description: The range of a subword of a word is a subset of the set of symbols for the word. (Contributed by AV, 13-Nov-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | swrdrn | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr 〈 𝑀 , 𝑁 〉 ) ⊆ 𝑉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | swrdf | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr 〈 𝑀 , 𝑁 〉 ) : ( 0 ..^ ( 𝑁 − 𝑀 ) ) ⟶ 𝑉 ) | |
2 | 1 | frnd | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr 〈 𝑀 , 𝑁 〉 ) ⊆ 𝑉 ) |