Description: The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | s2len | ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-s2 | ⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ ) | |
2 | s1cli | ⊢ ⟨“ 𝐴 ”⟩ ∈ Word V | |
3 | s1len | ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1 | |
4 | 1p1e2 | ⊢ ( 1 + 1 ) = 2 | |
5 | 1 2 3 4 | cats1len | ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2 |