Description: The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn . (Contributed by Thierry Arnoux, 12-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pfxrn2 | ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐿 ) ⊆ ran 𝑊 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pfxres | ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) = ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) ) | |
| 2 | 1 | rneqd | ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐿 ) = ran ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) ) |
| 3 | resss | ⊢ ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) ⊆ 𝑊 | |
| 4 | 3 | rnssi | ⊢ ran ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) ⊆ ran 𝑊 |
| 5 | 2 4 | eqsstrdi | ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐿 ) ⊆ ran 𝑊 ) |