Metamath Proof Explorer

Theorem cats1cli

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

Ref Expression
Hypotheses cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
cats1cli.2 ⊢ S ∈ Word V
Assertion cats1cli ⊢ T ∈ Word V

Proof

Step Hyp Ref Expression
1 cats1cld.1 ⊢ T = S ++ ⟨“ X ”⟩
2 cats1cli.2 ⊢ S ∈ Word V
3 s1cli ⊢ ⟨“ X ”⟩ ∈ Word V
4 ccatcl ⊢ S ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V → S ++ ⟨“ X ”⟩ ∈ Word V
5 2 3 4 mp2an ⊢ S ++ ⟨“ X ”⟩ ∈ Word V
6 1 5 eqeltri ⊢ T ∈ Word V