Metamath Proof Explorer


Theorem swrdrn

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 ⟨ 𝑀 , 𝑁 ⟩ ) ⊆ 𝑉 )

Proof

Step Hyp Ref Expression
1 swrdf ( ( 𝑊 ∈ Word 𝑉𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) : ( 0 ..^ ( 𝑁𝑀 ) ) ⟶ 𝑉 )
2 1 frnd ( ( 𝑊 ∈ Word 𝑉𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⊆ 𝑉 )