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