Metamath Proof Explorer

Theorem ccatws1clv

Description: The concatenation of a word with a singleton word (which can be over a different alphabet) is a word. (Contributed by AV, 5-Mar-2022)

Ref Expression
Assertion ccatws1clv ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ ∈ Word V

Proof

Step Hyp Ref Expression
1 wrdv ⊢ W ∈ Word V → W ∈ Word V
2 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
3 ccatcl ⊢ W ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V → W ++ ⟨“ X ”⟩ ∈ Word V
4 1 2 3 sylancl ⊢ W ∈ Word V → W ++ ⟨“ X ”⟩ ∈ Word V