wrdred1

Description: A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021)

		Ref	Expression
	Assertion	wrdred1	$⊢ F \in Word S \to {F ↾}_{(0 ..^\|F\| - 1)} \in Word S$

Step	Hyp	Ref	Expression
1		wrdf	$⊢ F \in Word S \to F : (0 ..^\|F\|) ⟶ S$
2		lencl	$⊢ F \in Word S \to \|F\| \in ℕ_{0}$
3		nn0z	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ$
4		fzossrbm1	$⊢ \|F\| \in ℤ \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
5	3 4	syl	$⊢ \|F\| \in ℕ_{0} \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
6		fssres	$⊢ (F : (0 ..^\|F\|) ⟶ S \land (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)) \to ({F ↾}_{(0 ..^\|F\| - 1)}) : (0 ..^\|F\| - 1) ⟶ S$
7	5 6	sylan2	$⊢ (F : (0 ..^\|F\|) ⟶ S \land \|F\| \in ℕ_{0}) \to ({F ↾}_{(0 ..^\|F\| - 1)}) : (0 ..^\|F\| - 1) ⟶ S$
8		iswrdi	$⊢ ({F ↾}_{(0 ..^\|F\| - 1)}) : (0 ..^\|F\| - 1) ⟶ S \to {F ↾}_{(0 ..^\|F\| - 1)} \in Word S$
9	7 8	syl	$⊢ (F : (0 ..^\|F\|) ⟶ S \land \|F\| \in ℕ_{0}) \to {F ↾}_{(0 ..^\|F\| - 1)} \in Word S$
10	1 2 9	syl2anc	$⊢ F \in Word S \to {F ↾}_{(0 ..^\|F\| - 1)} \in Word S$

Metamath Proof Explorer