Step |
Hyp |
Ref |
Expression |
1 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
2 |
1
|
a1i |
⊢ ( 𝑊 ≠ ∅ → 1 ∈ ℕ0 ) |
3 |
|
pfxval |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ∈ ℕ0 ) → ( 𝑊 prefix 1 ) = ( 𝑊 substr 〈 0 , 1 〉 ) ) |
4 |
2 3
|
sylan2 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 prefix 1 ) = ( 𝑊 substr 〈 0 , 1 〉 ) ) |
5 |
|
1e0p1 |
⊢ 1 = ( 0 + 1 ) |
6 |
5
|
opeq2i |
⊢ 〈 0 , 1 〉 = 〈 0 , ( 0 + 1 ) 〉 |
7 |
6
|
oveq2i |
⊢ ( 𝑊 substr 〈 0 , 1 〉 ) = ( 𝑊 substr 〈 0 , ( 0 + 1 ) 〉 ) |
8 |
7
|
a1i |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 substr 〈 0 , 1 〉 ) = ( 𝑊 substr 〈 0 , ( 0 + 1 ) 〉 ) ) |
9 |
|
lennncl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ ) |
10 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) |
11 |
9 10
|
sylibr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
12 |
|
swrds1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr 〈 0 , ( 0 + 1 ) 〉 ) = 〈“ ( 𝑊 ‘ 0 ) ”〉 ) |
13 |
11 12
|
syldan |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 substr 〈 0 , ( 0 + 1 ) 〉 ) = 〈“ ( 𝑊 ‘ 0 ) ”〉 ) |
14 |
4 8 13
|
3eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 prefix 1 ) = 〈“ ( 𝑊 ‘ 0 ) ”〉 ) |