Metamath Proof Explorer


Theorem pfxrn3

Description: Express the range of a prefix of a word. Stronger version of pfxrn2 . (Contributed by Thierry Arnoux, 13-Dec-2023)

Ref Expression
Assertion pfxrn3 W Word S L 0 W ran W prefix L = W 0 ..^ L

Proof

Step Hyp Ref Expression
1 pfxres W Word S L 0 W W prefix L = W 0 ..^ L
2 1 rneqd W Word S L 0 W ran W prefix L = ran W 0 ..^ L
3 df-ima W 0 ..^ L = ran W 0 ..^ L
4 2 3 eqtr4di W Word S L 0 W ran W prefix L = W 0 ..^ L