Theorem pfxrn2

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

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		resss	|- ( W |` ( 0 ..^ L ) ) C_ W
4	3	rnssi	|- ran ( W |` ( 0 ..^ L ) ) C_ ran W
5	2 4	eqsstrdi	|- ( ( W e. Word S /\ L e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix L ) C_ ran W )