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	|- ( ( W e. Word S /\ L e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix L ) = ( W " ( 0 ..^ L ) ) )

Proof

Step	Hyp	Ref	Expression
1		pfxres	|- ( ( W e. Word S /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) = ( W |` ( 0 ..^ L ) ) )
2	1	rneqd	|- ( ( W e. Word S /\ L e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix L ) = ran ( W |` ( 0 ..^ L ) ) )
3		df-ima	|- ( W " ( 0 ..^ L ) ) = ran ( W |` ( 0 ..^ L ) )
4	2 3	eqtr4di	|- ( ( W e. Word S /\ L e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix L ) = ( W " ( 0 ..^ L ) ) )