Theorem cats1cld

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

	Ref	Expression
Hypotheses	cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
	cats1cld.2	⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
	cats1cld.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion	cats1cld	⊢ ( 𝜑 → 𝑇 ∈ Word 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
2		cats1cld.2	⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
3		cats1cld.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4	3	s1cld	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ Word 𝐴 )
5		ccatcl	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝐴 ) → ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝐴 )
6	2 4 5	syl2anc	⊢ ( 𝜑 → ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝐴 )
7	1 6	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ Word 𝐴 )