Description: Reverse closure of a concatenation: If the concatenation of two arbitrary words is a word over an alphabet then the symbols of the first word belong to the alphabet. (Contributed by AV, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | ccatrcl1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 | |
|
2 | wrdv | |
|
3 | wrdv | |
|
4 | ccatalpha | |
|
5 | 2 3 4 | syl2an | |
6 | 1 5 | sylan9bbr | |
7 | simpl | |
|
8 | 6 7 | syl6bi | |
9 | 8 | expimpd | |
10 | 9 | 3impia | |