Metamath Proof Explorer
Description: The concatenation of a word with a singleton word (which can be over a
different alphabet) is a word. (Contributed by AV, 5-Mar-2022)
|
|
Ref |
Expression |
|
Assertion |
ccatws1clv |
⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ∈ Word V ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
wrdv |
⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V ) |
2 |
|
s1cli |
⊢ 〈“ 𝑋 ”〉 ∈ Word V |
3 |
|
ccatcl |
⊢ ( ( 𝑊 ∈ Word V ∧ 〈“ 𝑋 ”〉 ∈ Word V ) → ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ∈ Word V ) |
4 |
1 2 3
|
sylancl |
⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ∈ Word V ) |