Description: The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 28-Sep-2018) (Proof shortened by AV, 14-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fstwrdne | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wrdlenge1n0 | ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑊 ) ) ) | |
| 2 | wrdsymb1 | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) | |
| 3 | 2 | ex | ⊢ ( 𝑊 ∈ Word 𝑉 → ( 1 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) ) |
| 4 | 1 3 | sylbid | ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ≠ ∅ → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) ) |
| 5 | 4 | imp | ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |