Metamath Proof Explorer


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