Metamath Proof Explorer

Theorem ccats1alpha

Description: A concatenation of a word with a singleton word is a word over an alphabet S iff the symbols of both words belong to the alphabet S . (Contributed by AV, 27-Mar-2022)

Ref Expression
Assertion ccats1alpha 
|- ( ( A e. Word V /\ X e. U ) -> ( ( A ++ <" X "> ) e. Word S <-> ( A e. Word S /\ X e. S ) ) )

Proof

Step Hyp Ref Expression
1 wrdv 
 |-  ( A e. Word V -> A e. Word _V )
2 s1cli 
 |-  <" X "> e. Word _V
3 2 a1i 
 |-  ( X e. U -> <" X "> e. Word _V )
4 ccatalpha 
 |-  ( ( A e. Word _V /\ <" X "> e. Word _V ) -> ( ( A ++ <" X "> ) e. Word S <-> ( A e. Word S /\ <" X "> e. Word S ) ) )
5 1 3 4 syl2an 
 |-  ( ( A e. Word V /\ X e. U ) -> ( ( A ++ <" X "> ) e. Word S <-> ( A e. Word S /\ <" X "> e. Word S ) ) )
6 simpr 
 |-  ( ( X e. U /\ <" X "> e. Word S ) -> <" X "> e. Word S )
7 s1len 
 |-  ( # ` <" X "> ) = 1
8 wrdl1exs1 
 |-  ( ( <" X "> e. Word S /\ ( # ` <" X "> ) = 1 ) -> E. w e. S <" X "> = <" w "> )
9 6 7 8 sylancl 
 |-  ( ( X e. U /\ <" X "> e. Word S ) -> E. w e. S <" X "> = <" w "> )
10 elex 
 |-  ( X e. U -> X e. _V )
11 10 adantr 
 |-  ( ( X e. U /\ <" X "> e. Word S ) -> X e. _V )
12 elex 
 |-  ( w e. S -> w e. _V )
13 s111 
 |-  ( ( X e. _V /\ w e. _V ) -> ( <" X "> = <" w "> <-> X = w ) )
14 11 12 13 syl2an 
 |-  ( ( ( X e. U /\ <" X "> e. Word S ) /\ w e. S ) -> ( <" X "> = <" w "> <-> X = w ) )
15 simpr 
 |-  ( ( ( X e. U /\ <" X "> e. Word S ) /\ w e. S ) -> w e. S )
16 eleq1 
 |-  ( X = w -> ( X e. S <-> w e. S ) )
17 15 16 syl5ibrcom 
 |-  ( ( ( X e. U /\ <" X "> e. Word S ) /\ w e. S ) -> ( X = w -> X e. S ) )
18 14 17 sylbid 
 |-  ( ( ( X e. U /\ <" X "> e. Word S ) /\ w e. S ) -> ( <" X "> = <" w "> -> X e. S ) )
19 18 rexlimdva 
 |-  ( ( X e. U /\ <" X "> e. Word S ) -> ( E. w e. S <" X "> = <" w "> -> X e. S ) )
20 9 19 mpd 
 |-  ( ( X e. U /\ <" X "> e. Word S ) -> X e. S )
21 20 ex 
 |-  ( X e. U -> ( <" X "> e. Word S -> X e. S ) )
22 s1cl 
 |-  ( X e. S -> <" X "> e. Word S )
23 21 22 impbid1 
 |-  ( X e. U -> ( <" X "> e. Word S <-> X e. S ) )
24 23 anbi2d 
 |-  ( X e. U -> ( ( A e. Word S /\ <" X "> e. Word S ) <-> ( A e. Word S /\ X e. S ) ) )
25 24 adantl 
 |-  ( ( A e. Word V /\ X e. U ) -> ( ( A e. Word S /\ <" X "> e. Word S ) <-> ( A e. Word S /\ X e. S ) ) )
26 5 25 bitrd 
 |-  ( ( A e. Word V /\ X e. U ) -> ( ( A ++ <" X "> ) e. Word S <-> ( A e. Word S /\ X e. S ) ) )