wrdres

Description: Condition for the restriction of a word to be a word itself. (Contributed by Thierry Arnoux, 5-Oct-2018)

		Ref	Expression
	Assertion	wrdres	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to {W ↾}_{(0 ..^N)} \in Word S$

Step	Hyp	Ref	Expression
1		wrdf	$⊢ W \in Word S \to W : (0 ..^\|W\|) ⟶ S$
2		elfzuz3	$⊢ N \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq N}$
3		fzoss2	$⊢ \|W\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|W\|)$
4	2 3	syl	$⊢ N \in (0 \dots \|W\|) \to (0 ..^N) \subseteq (0 ..^\|W\|)$
5		fssres	$⊢ (W : (0 ..^\|W\|) ⟶ S \land (0 ..^N) \subseteq (0 ..^\|W\|)) \to ({W ↾}_{(0 ..^N)}) : (0 ..^N) ⟶ S$
6	1 4 5	syl2an	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to ({W ↾}_{(0 ..^N)}) : (0 ..^N) ⟶ S$
7		iswrdi	$⊢ ({W ↾}_{(0 ..^N)}) : (0 ..^N) ⟶ S \to {W ↾}_{(0 ..^N)} \in Word S$
8	6 7	syl	$⊢ (W \in Word S \land N \in (0 \dots \|W\|)) \to {W ↾}_{(0 ..^N)} \in Word S$

Metamath Proof Explorer