Metamath Proof Explorer

Theorem pfxrn

Description: The range of a prefix of a word is a subset of the set of symbols for the word. (Contributed by AV, 2-May-2020)

		Ref	Expression
	Assertion	pfxrn	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to ran (W prefix L) \subseteq V$

Step	Hyp	Ref	Expression
1		pfxf	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to (W prefix L) : (0 ..^L) ⟶ V$
2	1	frnd	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to ran (W prefix L) \subseteq V$