iswrdi

Description: A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

		Ref	Expression
	Assertion	iswrdi	$⊢ W : (0 ..^L) ⟶ S \to W \in Word S$

Step	Hyp	Ref	Expression
1		oveq2	$⊢ l = L \to (0 ..^l) = (0 ..^L)$
2	1	feq2d	$⊢ l = L \to (W : (0 ..^l) ⟶ S \leftrightarrow W : (0 ..^L) ⟶ S)$
3	2	rspcev	$⊢ (L \in ℕ_{0} \land W : (0 ..^L) ⟶ S) \to \exists l \in ℕ_{0} W : (0 ..^l) ⟶ S$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5		fzo0n0	$⊢ (0 ..^L) \neq \emptyset \leftrightarrow L \in ℕ$
6		nnnn0	$⊢ L \in ℕ \to L \in ℕ_{0}$
7	5 6	sylbi	$⊢ (0 ..^L) \neq \emptyset \to L \in ℕ_{0}$
8	7	necon1bi	$⊢ \neg L \in ℕ_{0} \to (0 ..^L) = \emptyset$
9		fzo0	$⊢ (0 ..^0) = \emptyset$
10	8 9	eqtr4di	$⊢ \neg L \in ℕ_{0} \to (0 ..^L) = (0 ..^0)$
11	10	feq2d	$⊢ \neg L \in ℕ_{0} \to (W : (0 ..^L) ⟶ S \leftrightarrow W : (0 ..^0) ⟶ S)$
12	11	biimpa	$⊢ (\neg L \in ℕ_{0} \land W : (0 ..^L) ⟶ S) \to W : (0 ..^0) ⟶ S$
13		oveq2	$⊢ l = 0 \to (0 ..^l) = (0 ..^0)$
14	13	feq2d	$⊢ l = 0 \to (W : (0 ..^l) ⟶ S \leftrightarrow W : (0 ..^0) ⟶ S)$
15	14	rspcev	$⊢ (0 \in ℕ_{0} \land W : (0 ..^0) ⟶ S) \to \exists l \in ℕ_{0} W : (0 ..^l) ⟶ S$
16	4 12 15	sylancr	$⊢ (\neg L \in ℕ_{0} \land W : (0 ..^L) ⟶ S) \to \exists l \in ℕ_{0} W : (0 ..^l) ⟶ S$
17	3 16	pm2.61ian	$⊢ W : (0 ..^L) ⟶ S \to \exists l \in ℕ_{0} W : (0 ..^l) ⟶ S$
18		iswrd	$⊢ W \in Word S \leftrightarrow \exists l \in ℕ_{0} W : (0 ..^l) ⟶ S$
19	17 18	sylibr	$⊢ W : (0 ..^L) ⟶ S \to W \in Word S$

Metamath Proof Explorer