Theorem 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	⊢ ( 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑙 = 𝐿 → ( 0 ..^ 𝑙 ) = ( 0 ..^ 𝐿 ) )
2	1	feq2d	⊢ ( 𝑙 = 𝐿 → ( 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) )
3	2	rspcev	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) → ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
4		0nn0	⊢ 0 ∈ ℕ0
5		fzo0n0	⊢ ( ( 0 ..^ 𝐿 ) ≠ ∅ ↔ 𝐿 ∈ ℕ )
6		nnnn0	⊢ ( 𝐿 ∈ ℕ → 𝐿 ∈ ℕ0 )
7	5 6	sylbi	⊢ ( ( 0 ..^ 𝐿 ) ≠ ∅ → 𝐿 ∈ ℕ0 )
8	7	necon1bi	⊢ ( ¬ 𝐿 ∈ ℕ0 → ( 0 ..^ 𝐿 ) = ∅ )
9		fzo0	⊢ ( 0 ..^ 0 ) = ∅
10	8 9	eqtr4di	⊢ ( ¬ 𝐿 ∈ ℕ0 → ( 0 ..^ 𝐿 ) = ( 0 ..^ 0 ) )
11	10	feq2d	⊢ ( ¬ 𝐿 ∈ ℕ0 → ( 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 ) )
12	11	biimpa	⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) → 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 )
13		oveq2	⊢ ( 𝑙 = 0 → ( 0 ..^ 𝑙 ) = ( 0 ..^ 0 ) )
14	13	feq2d	⊢ ( 𝑙 = 0 → ( 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 ) )
15	14	rspcev	⊢ ( ( 0 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 ) → ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
16	4 12 15	sylancr	⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) → ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
17	3 16	pm2.61ian	⊢ ( 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 → ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
18		iswrd	⊢ ( 𝑊 ∈ Word 𝑆 ↔ ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
19	17 18	sylibr	⊢ ( 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )