Theorem 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	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		wrdf	⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
2		elfzuz3	⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
3		fzoss2	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
4	2 3	syl	⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5		fssres	⊢ ( ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 ∧ ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
6	1 4 5	syl2an	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
7		iswrdi	⊢ ( ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) ⟶ 𝑆 → ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word 𝑆 )
8	6 7	syl	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word 𝑆 )