Metamath Proof Explorer


Theorem ccat2s1cl

Description: The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018)

Ref Expression
Assertion ccat2s1cl
|- ( ( X e. V /\ Y e. V ) -> ( <" X "> ++ <" Y "> ) e. Word V )

Proof

Step Hyp Ref Expression
1 s1cl
 |-  ( X e. V -> <" X "> e. Word V )
2 ccatws1cl
 |-  ( ( <" X "> e. Word V /\ Y e. V ) -> ( <" X "> ++ <" Y "> ) e. Word V )
3 1 2 sylan
 |-  ( ( X e. V /\ Y e. V ) -> ( <" X "> ++ <" Y "> ) e. Word V )