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 )