Theorem cats1cli

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

	Ref	Expression
Hypotheses	cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
	cats1cli.2	⊢ 𝑆 ∈ Word V
Assertion	cats1cli	⊢ 𝑇 ∈ Word V

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
2		cats1cli.2	⊢ 𝑆 ∈ Word V
3		s1cli	⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
4		ccatcl	⊢ ( ( 𝑆 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ) → ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V )
5	2 3 4	mp2an	⊢ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word V
6	1 5	eqeltri	⊢ 𝑇 ∈ Word V