This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )