Step |
Hyp |
Ref |
Expression |
1 |
|
fzval3 |
⊢ ( 𝐿 ∈ ℤ → ( 0 ... 𝐿 ) = ( 0 ..^ ( 𝐿 + 1 ) ) ) |
2 |
1
|
feq2d |
⊢ ( 𝐿 ∈ ℤ → ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ ( 𝐿 + 1 ) ) ⟶ 𝑆 ) ) |
3 |
|
iswrdi |
⊢ ( 𝑊 : ( 0 ..^ ( 𝐿 + 1 ) ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 ) |
4 |
2 3
|
syl6bi |
⊢ ( 𝐿 ∈ ℤ → ( 𝑊 : ( 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
|
syl6bi |
⊢ ( ¬ 𝐿 ∈ ℤ → ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 ) ) |
13 |
4 12
|
pm2.61i |
⊢ ( 𝑊 : ( 0 ... 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 ) |