Metamath Proof Explorer

Theorem swrdrn

Description: The range of a subword of a word is a subset of the set of symbols for the word. (Contributed by AV, 13-Nov-2018)

		Ref	Expression
	Assertion	swrdrn	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) \subseteq V$

Step	Hyp	Ref	Expression
1		swrdf	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to (W substr ⟨M, N⟩) : (0 ..^N - M) ⟶ V$
2	1	frnd	$⊢ (W \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|W\|)) \to ran (W substr ⟨M, N⟩) \subseteq V$