This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Extract the first symbol from a doubleton word. (Contributed by Stefan
O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)
|
|
Ref |
Expression |
|
Assertion |
s2fv0 |
⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) = 𝐴 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-s2 |
⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) |
| 2 |
|
s1cli |
⊢ ⟨“ 𝐴 ”⟩ ∈ Word V |
| 3 |
|
s1len |
⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1 |
| 4 |
|
s1fv |
⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) = 𝐴 ) |
| 5 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
| 6 |
|
0lt1 |
⊢ 0 < 1 |
| 7 |
1 2 3 4 5 6
|
cats1fv |
⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) = 𝐴 ) |