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 ) |
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 ) |