Metamath Proof Explorer

Theorem ccat2s1cl

Description: The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018)

Ref Expression
Assertion ccat2s1cl ⊢ X ∈ V ∧ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V

Proof

Step Hyp Ref Expression
1 s1cl ⊢ X ∈ V → ⟨“ X ”⟩ ∈ Word V
2 ccatws1cl ⊢ ⟨“ X ”⟩ ∈ Word V ∧ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V
3 1 2 sylan ⊢ X ∈ V ∧ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ∈ Word V