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 ) |