Metamath Proof Explorer
Description: The range of a prefix of a word is a subset of the set of symbols for the
word. (Contributed by AV, 2-May-2020)
|
|
Ref |
Expression |
|
Assertion |
pfxrn |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐿 ) ⊆ 𝑉 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pfxf |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) : ( 0 ..^ 𝐿 ) ⟶ 𝑉 ) |
| 2 |
1
|
frnd |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐿 ) ⊆ 𝑉 ) |