Description: A prefix of a word is a function from a half-open range of nonnegative integers of the same length as the prefix to the set of symbols for the original word. (Contributed by AV, 2-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | pfxf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pfxmpt | |
|
2 | simpll | |
|
3 | elfzuz3 | |
|
4 | 3 | adantl | |
5 | fzoss2 | |
|
6 | 4 5 | syl | |
7 | 6 | sselda | |
8 | wrdsymbcl | |
|
9 | 2 7 8 | syl2anc | |
10 | 1 9 | fmpt3d | |