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 ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V )

Proof

Step Hyp Ref Expression
1 wrdv ( 𝑊 ∈ Word 𝑉𝑊 ∈ Word V )
2 s1cli ⟨“ 𝑋 ”⟩ ∈ Word V
3 ccatcl ( ( 𝑊 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ) → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V )
4 1 2 3 sylancl ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V )