Theorem cats1cld

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

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

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	|- T = ( S ++ <" X "> )
2		cats1cld.2	|- ( ph -> S e. Word A )
3		cats1cld.3	|- ( ph -> X e. A )
4	3	s1cld	|- ( ph -> <" X "> e. Word A )
5		ccatcl	|- ( ( S e. Word A /\ <" X "> e. Word A ) -> ( S ++ <" X "> ) e. Word A )
6	2 4 5	syl2anc	|- ( ph -> ( S ++ <" X "> ) e. Word A )
7	1 6	eqeltrid	|- ( ph -> T e. Word A )