Metamath Proof Explorer

Theorem ccat2s1lenOLD

Description: Obsolete version of ccat2s1len as of 14-Jan-2024. The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ccat2s1lenOLD ⊢ X ∈ V ∧ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = 2

Proof

Step Hyp Ref Expression
1 s1cl ⊢ X ∈ V → ⟨“ X ”⟩ ∈ Word V
2 s1cl ⊢ Y ∈ V → ⟨“ Y ”⟩ ∈ Word V
3 ccatlenOLD ⊢ ⟨“ X ”⟩ ∈ Word V ∧ ⟨“ Y ”⟩ ∈ Word V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = ⟨“ X ”⟩ + ⟨“ Y ”⟩
4 s1len ⊢ ⟨“ X ”⟩ = 1
5 s1len ⊢ ⟨“ Y ”⟩ = 1
6 4 5 oveq12i ⊢ ⟨“ X ”⟩ + ⟨“ Y ”⟩ = 1 + 1
7 1p1e2 ⊢ 1 + 1 = 2
8 6 7 eqtri ⊢ ⟨“ X ”⟩ + ⟨“ Y ”⟩ = 2
9 3 8 eqtrdi ⊢ ⟨“ X ”⟩ ∈ Word V ∧ ⟨“ Y ”⟩ ∈ Word V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = 2
10 1 2 9 syl2an ⊢ X ∈ V ∧ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = 2