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 ∈ Word X ∧ B ∈ Word Y ∧ W = A ++ B ∧ W ∈ Word S → A ∈ Word S

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ W = A ++ B → W ∈ Word S ↔ A ++ B ∈ Word S
2 wrdv ⊢ A ∈ Word X → A ∈ Word V
3 wrdv ⊢ B ∈ Word Y → B ∈ Word V
4 ccatalpha ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B ∈ Word S ↔ A ∈ Word S ∧ B ∈ Word S
5 2 3 4 syl2an ⊢ A ∈ Word X ∧ B ∈ Word Y → A ++ B ∈ Word S ↔ A ∈ Word S ∧ B ∈ Word S
6 1 5 sylan9bbr ⊢ A ∈ Word X ∧ B ∈ Word Y ∧ W = A ++ B → W ∈ Word S ↔ A ∈ Word S ∧ B ∈ Word S
7 simpl ⊢ A ∈ Word S ∧ B ∈ Word S → A ∈ Word S
8 6 7 biimtrdi ⊢ A ∈ Word X ∧ B ∈ Word Y ∧ W = A ++ B → W ∈ Word S → A ∈ Word S
9 8 expimpd ⊢ A ∈ Word X ∧ B ∈ Word Y → W = A ++ B ∧ W ∈ Word S → A ∈ Word S
10 9 3impia ⊢ A ∈ Word X ∧ B ∈ Word Y ∧ W = A ++ B ∧ W ∈ Word S → A ∈ Word S