This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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