Theorem pfxrn3

Description: Express the range of a prefix of a word. Stronger version of pfxrn2 . (Contributed by Thierry Arnoux, 13-Dec-2023)

	Ref	Expression
Assertion	pfxrn3	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐿 ) = ( 𝑊 “ ( 0 ..^ 𝐿 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pfxres	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) = ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) )
2	1	rneqd	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐿 ) = ran ( 𝑊 ↾ ( 0 ..^ 𝐿 ) ) )
3		df-ima	⊢ ( 𝑊 “ ( 0 ..^ 𝐿 ) ) = ran ( 𝑊 ↾ ( 0 ..^ 𝐿 ) )
4	2 3	eqtr4di	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐿 ) = ( 𝑊 “ ( 0 ..^ 𝐿 ) ) )