Theorem cats1cli

Description: Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Hypotheses	cats1cld.1	|- T = ( S ++ <" X "> )
	cats1cli.2	|- S e. Word _V
Assertion	cats1cli	|- T e. Word _V

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	|- T = ( S ++ <" X "> )
2		cats1cli.2	|- S e. Word _V
3		s1cli	|- <" X "> e. Word _V
4		ccatcl	|- ( ( S e. Word _V /\ <" X "> e. Word _V ) -> ( S ++ <" X "> ) e. Word _V )
5	2 3 4	mp2an	|- ( S ++ <" X "> ) e. Word _V
6	1 5	eqeltri	|- T e. Word _V