Metamath Proof Explorer


Theorem ccatrcl1

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 AWordXBWordYW=A++BWWordSAWordS

Proof

Step Hyp Ref Expression
1 eleq1 W=A++BWWordSA++BWordS
2 wrdv AWordXAWordV
3 wrdv BWordYBWordV
4 ccatalpha AWordVBWordVA++BWordSAWordSBWordS
5 2 3 4 syl2an AWordXBWordYA++BWordSAWordSBWordS
6 1 5 sylan9bbr AWordXBWordYW=A++BWWordSAWordSBWordS
7 simpl AWordSBWordSAWordS
8 6 7 syl6bi AWordXBWordYW=A++BWWordSAWordS
9 8 expimpd AWordXBWordYW=A++BWWordSAWordS
10 9 3impia AWordXBWordYW=A++BWWordSAWordS