Metamath Proof Explorer


Theorem pfxf

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 WWordVL0WWprefixL:0..^LV

Proof

Step Hyp Ref Expression
1 pfxmpt WWordVL0WWprefixL=x0..^LWx
2 simpll WWordVL0Wx0..^LWWordV
3 elfzuz3 L0WWL
4 3 adantl WWordVL0WWL
5 fzoss2 WL0..^L0..^W
6 4 5 syl WWordVL0W0..^L0..^W
7 6 sselda WWordVL0Wx0..^Lx0..^W
8 wrdsymbcl WWordVx0..^WWxV
9 2 7 8 syl2anc WWordVL0Wx0..^LWxV
10 1 9 fmpt3d WWordVL0WWprefixL:0..^LV