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 e. Word V -> ( W ++ <" X "> ) e. Word _V )

Proof

Step	Hyp	Ref	Expression
1		wrdv	|- ( W e. Word V -> W e. Word _V )
2		s1cli	|- <" X "> e. Word _V
3		ccatcl	|- ( ( W e. Word _V /\ <" X "> e. Word _V ) -> ( W ++ <" X "> ) e. Word _V )
4	1 2 3	sylancl	|- ( W e. Word V -> ( W ++ <" X "> ) e. Word _V )