Step |
Hyp |
Ref |
Expression |
1 |
|
simprl |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → 𝑊 ∈ Word 𝑉 ) |
2 |
|
nnge1 |
⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 ) |
3 |
2
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → 1 ≤ 𝑁 ) |
4 |
|
breq2 |
⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 1 ≤ ( ♯ ‘ 𝑊 ) ↔ 1 ≤ 𝑁 ) ) |
5 |
4
|
ad2antll |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → ( 1 ≤ ( ♯ ‘ 𝑊 ) ↔ 1 ≤ 𝑁 ) ) |
6 |
3 5
|
mpbird |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → 1 ≤ ( ♯ ‘ 𝑊 ) ) |
7 |
|
wrdsymb1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |
8 |
1 6 7
|
syl2anc |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |