Metamath Proof Explorer

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 \in Word S \land L \in (0 \dots \|W\|)) \to ran (W prefix L) \subseteq ran W$

Proof

Step	Hyp	Ref	Expression
1		pfxres	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to W prefix L = {W ↾}_{(0 ..^L)}$
2	1	rneqd	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to ran (W prefix L) = ran ({W ↾}_{(0 ..^L)})$
3		resss	$⊢ {W ↾}_{(0 ..^L)} \subseteq W$
4	3	rnssi	$⊢ ran ({W ↾}_{(0 ..^L)}) \subseteq ran W$
5	2 4	eqsstrdi	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to ran (W prefix L) \subseteq ran W$