This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A e. Word X /\ B e. Word Y /\ ( W = ( A ++ B ) /\ W e. Word S ) ) -> A e. Word S )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( W = ( A ++ B ) -> ( W e. Word S <-> ( A ++ B ) e. Word S ) )
2 wrdv 
 |-  ( A e. Word X -> A e. Word _V )
3 wrdv 
 |-  ( B e. Word Y -> B e. Word _V )
4 ccatalpha 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( A ++ B ) e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )
5 2 3 4 syl2an 
 |-  ( ( A e. Word X /\ B e. Word Y ) -> ( ( A ++ B ) e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )
6 1 5 sylan9bbr 
 |-  ( ( ( A e. Word X /\ B e. Word Y ) /\ W = ( A ++ B ) ) -> ( W e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )
7 simpl 
 |-  ( ( A e. Word S /\ B e. Word S ) -> A e. Word S )
8 6 7 biimtrdi 
 |-  ( ( ( A e. Word X /\ B e. Word Y ) /\ W = ( A ++ B ) ) -> ( W e. Word S -> A e. Word S ) )
9 8 expimpd 
 |-  ( ( A e. Word X /\ B e. Word Y ) -> ( ( W = ( A ++ B ) /\ W e. Word S ) -> A e. Word S ) )
10 9 3impia 
 |-  ( ( A e. Word X /\ B e. Word Y /\ ( W = ( A ++ B ) /\ W e. Word S ) ) -> A e. Word S )