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	$⊢ W : (0 \dots L) ⟶ S \to W \in Word S$

Proof

Step	Hyp	Ref	Expression
1		fzval3	$⊢ L \in ℤ \to (0 \dots L) = (0 ..^L + 1)$
2	1	feq2d	$⊢ L \in ℤ \to (W : (0 \dots L) ⟶ S \leftrightarrow W : (0 ..^L + 1) ⟶ S)$
3		iswrdi	$⊢ W : (0 ..^L + 1) ⟶ S \to W \in Word S$
4	2 3	biimtrdi	$⊢ L \in ℤ \to (W : (0 \dots L) ⟶ S \to W \in Word S)$
5		fzn0	$⊢ (0 \dots L) \neq \emptyset \leftrightarrow L \in ℤ_{\geq 0}$
6		elnn0uz	$⊢ L \in ℕ_{0} \leftrightarrow L \in ℤ_{\geq 0}$
7	5 6	sylbb2	$⊢ (0 \dots L) \neq \emptyset \to L \in ℕ_{0}$
8	7	nn0zd	$⊢ (0 \dots L) \neq \emptyset \to L \in ℤ$
9	8	necon1bi	$⊢ \neg L \in ℤ \to (0 \dots L) = \emptyset$
10	9	feq2d	$⊢ \neg L \in ℤ \to (W : (0 \dots L) ⟶ S \leftrightarrow W : \emptyset ⟶ S)$
11		iswrddm0	$⊢ W : \emptyset ⟶ S \to W \in Word S$
12	10 11	biimtrdi	$⊢ \neg L \in ℤ \to (W : (0 \dots L) ⟶ S \to W \in Word S)$
13	4 12	pm2.61i	$⊢ W : (0 \dots L) ⟶ S \to W \in Word S$