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 𝑆 )