Metamath Proof Explorer


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 )