Theorem cats1cli

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

	Ref	Expression
Hypotheses	cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
	cats1cli.2	$$⊢S\in \mathrm{Word}\mathrm{V}$$
Assertion	cats1cli	$$⊢T\in \mathrm{Word}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
2		cats1cli.2	$$⊢S\in \mathrm{Word}\mathrm{V}$$
3		s1cli	$$⊢⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
4		ccatcl	$$⊢\left(S\in \mathrm{Word}\mathrm{V}\wedge ⟨“X”⟩\in \mathrm{Word}\mathrm{V}\right)\to S\mathrm{++}⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
5	2 3 4	mp2an	$$⊢S\mathrm{++}⟨“X”⟩\in \mathrm{Word}\mathrm{V}$$
6	1 5	eqeltri	$$⊢T\in \mathrm{Word}\mathrm{V}$$