Theorem cats1cld

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

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

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	$$⊢T=S\mathrm{++}⟨“X”⟩$$
2		cats1cld.2	$$⊢\phi \to S\in \mathrm{Word}A$$
3		cats1cld.3	$$⊢\phi \to X\in A$$
4	3	s1cld	$$⊢\phi \to ⟨“X”⟩\in \mathrm{Word}A$$
5		ccatcl	$$⊢\left(S\in \mathrm{Word}A\wedge ⟨“X”⟩\in \mathrm{Word}A\right)\to S\mathrm{++}⟨“X”⟩\in \mathrm{Word}A$$
6	2 4 5	syl2anc	$$⊢\phi \to S\mathrm{++}⟨“X”⟩\in \mathrm{Word}A$$
7	1 6	eqeltrid	$$⊢\phi \to T\in \mathrm{Word}A$$