Metamath Proof Explorer


Theorem wrdfd

Description: A word is a zero-based sequence with a recoverable upper limit, deduction version. (Contributed by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Hypotheses wrdfd.n φ N = W
wrdfd.w φ W Word S
Assertion wrdfd φ W : 0 ..^ N S

Proof

Step Hyp Ref Expression
1 wrdfd.n φ N = W
2 wrdfd.w φ W Word S
3 wrdf W Word S W : 0 ..^ W S
4 2 3 syl φ W : 0 ..^ W S
5 1 oveq2d φ 0 ..^ N = 0 ..^ W
6 5 feq2d φ W : 0 ..^ N S W : 0 ..^ W S
7 4 6 mpbird φ W : 0 ..^ N S