Metamath Proof Explorer

Theorem ccats1pfxeqrex

Description: There exists a symbol such that its concatenation after the prefix obtained by deleting the last symbol of a nonempty word results in the word itself. (Contributed by AV, 5-Oct-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion ccats1pfxeqrex 
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> E. s e. V U = ( W ++ <" s "> ) ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> U e. Word V )
2 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
3 2 3ad2ant1 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( # ` W ) e. NN0 )
4 nn0p1nn 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) + 1 ) e. NN )
5 nngt0 
 |-  ( ( ( # ` W ) + 1 ) e. NN -> 0 < ( ( # ` W ) + 1 ) )
6 3 4 5 3syl 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> 0 < ( ( # ` W ) + 1 ) )
7 breq2 
 |-  ( ( # ` U ) = ( ( # ` W ) + 1 ) -> ( 0 < ( # ` U ) <-> 0 < ( ( # ` W ) + 1 ) ) )
8 7 3ad2ant3 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( 0 < ( # ` U ) <-> 0 < ( ( # ` W ) + 1 ) ) )
9 6 8 mpbird 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> 0 < ( # ` U ) )
10 hashgt0n0 
 |-  ( ( U e. Word V /\ 0 < ( # ` U ) ) -> U =/= (/) )
11 1 9 10 syl2anc 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> U =/= (/) )
12 lswcl 
 |-  ( ( U e. Word V /\ U =/= (/) ) -> ( lastS ` U ) e. V )
13 1 11 12 syl2anc 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( lastS ` U ) e. V )
14 ccats1pfxeq 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" ( lastS ` U ) "> ) ) )
15 s1eq 
 |-  ( s = ( lastS ` U ) -> <" s "> = <" ( lastS ` U ) "> )
16 15 oveq2d 
 |-  ( s = ( lastS ` U ) -> ( W ++ <" s "> ) = ( W ++ <" ( lastS ` U ) "> ) )
17 16 rspceeqv 
 |-  ( ( ( lastS ` U ) e. V /\ U = ( W ++ <" ( lastS ` U ) "> ) ) -> E. s e. V U = ( W ++ <" s "> ) )
18 13 14 17 syl6an 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> E. s e. V U = ( W ++ <" s "> ) ) )