Metamath Proof Explorer


Theorem wrdred1

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

Ref Expression
Assertion wrdred1
|- ( F e. Word S -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word S )

Proof

Step Hyp Ref Expression
1 wrdf
 |-  ( F e. Word S -> F : ( 0 ..^ ( # ` F ) ) --> S )
2 lencl
 |-  ( F e. Word S -> ( # ` F ) e. NN0 )
3 nn0z
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ZZ )
4 fzossrbm1
 |-  ( ( # ` F ) e. ZZ -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
5 3 4 syl
 |-  ( ( # ` F ) e. NN0 -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
6 fssres
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) --> S /\ ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) : ( 0 ..^ ( ( # ` F ) - 1 ) ) --> S )
7 5 6 sylan2
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) --> S /\ ( # ` F ) e. NN0 ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) : ( 0 ..^ ( ( # ` F ) - 1 ) ) --> S )
8 iswrdi
 |-  ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) : ( 0 ..^ ( ( # ` F ) - 1 ) ) --> S -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word S )
9 7 8 syl
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) --> S /\ ( # ` F ) e. NN0 ) -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word S )
10 1 2 9 syl2anc
 |-  ( F e. Word S -> ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) e. Word S )