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	|- ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W |` ( 0 ..^ N ) ) e. Word S )

Proof

Step	Hyp	Ref	Expression
1		wrdf	|- ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S )
2		elfzuz3	|- ( N e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` N ) )
3		fzoss2	|- ( ( # ` W ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
4	2 3	syl	|- ( N e. ( 0 ... ( # ` W ) ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) )
5		fssres	|- ( ( W : ( 0 ..^ ( # ` W ) ) --> S /\ ( 0 ..^ N ) C_ ( 0 ..^ ( # ` W ) ) ) -> ( W |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S )
6	1 4 5	syl2an	|- ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S )
7		iswrdi	|- ( ( W |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S -> ( W |` ( 0 ..^ N ) ) e. Word S )
8	6 7	syl	|- ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W |` ( 0 ..^ N ) ) e. Word S )