Theorem wrdred1

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

	Ref	Expression
Assertion	wrdred1	⊢ ( 𝐹 ∈ Word 𝑆 → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		wrdf	⊢ ( 𝐹 ∈ Word 𝑆 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 )
2		lencl	⊢ ( 𝐹 ∈ Word 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
3		nn0z	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
4		fzossrbm1	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5	3 4	syl	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
6		fssres	⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 ∧ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑆 )
7	5 6	sylan2	⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑆 )
8		iswrdi	⊢ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑆 → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word 𝑆 )
9	7 8	syl	⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word 𝑆 )
10	1 2 9	syl2anc	⊢ ( 𝐹 ∈ Word 𝑆 → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word 𝑆 )