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

Metamath Proof Explorer

Theorem ffz0iswrd

Description: A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018) (Proof shortened by AV, 13-Oct-2018) (Proof shortened by JJ, 18-Nov-2022)

Ref Expression
Assertion ffz0iswrd ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )

Proof

Step Hyp Ref Expression
1 fzval3 ⊢ ( 𝐿 ∈ ℤ → ( 0 ... 𝐿 ) = ( 0 ..^ ( 𝐿 + 1 ) ) )
2 1 feq2d ⊢ ( 𝐿 ∈ ℤ → ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ ( 𝐿 + 1 ) ) ⟶ 𝑆 ) )
3 iswrdi ⊢ ( 𝑊 : ( 0 ..^ ( 𝐿 + 1 ) ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )
4 2 3 biimtrdi ⊢ ( 𝐿 ∈ ℤ → ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 ) )
5 fzn0 ⊢ ( ( 0 ... 𝐿 ) ≠ ∅ ↔ 𝐿 ∈ ( ℤ≥ ‘ 0 ) )
6 elnn0uz ⊢ ( 𝐿 ∈ ℕ0 ↔ 𝐿 ∈ ( ℤ≥ ‘ 0 ) )
7 5 6 sylbb2 ⊢ ( ( 0 ... 𝐿 ) ≠ ∅ → 𝐿 ∈ ℕ0 )
8 7 nn0zd ⊢ ( ( 0 ... 𝐿 ) ≠ ∅ → 𝐿 ∈ ℤ )
9 8 necon1bi ⊢ ( ¬ 𝐿 ∈ ℤ → ( 0 ... 𝐿 ) = ∅ )
10 9 feq2d ⊢ ( ¬ 𝐿 ∈ ℤ → ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 ↔ 𝑊 : ∅ ⟶ 𝑆 ) )
11 iswrddm0 ⊢ ( 𝑊 : ∅ ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )
12 10 11 biimtrdi ⊢ ( ¬ 𝐿 ∈ ℤ → ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 ) )
13 4 12 pm2.61i ⊢ ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )