This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → S ∈ Word A
cats1cld.3 ⊢ φ → X ∈ A
Assertion cats1cld ⊢ φ → T ∈ Word A

Proof

Step Hyp Ref Expression
1 cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
2 cats1cld.2 ⊢ φ → S ∈ Word A
3 cats1cld.3 ⊢ φ → X ∈ A
4 3 s1cld ⊢ φ → ⟨“ X ”⟩ ∈ Word A
5 ccatcl ⊢ S ∈ Word A ∧ ⟨“ X ”⟩ ∈ Word A → S ++ ⟨“ X ”⟩ ∈ Word A
6 2 4 5 syl2anc ⊢ φ → S ++ ⟨“ X ”⟩ ∈ Word A
7 1 6 eqeltrid ⊢ φ → T ∈ Word A