Metamath Proof Explorer


Theorem reuccatpfxs1v

Description: There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 21-Jan-2022) (Revised by AV, 10-May-2022) (Proof shortened by AV, 13-Oct-2022)

Ref Expression
Assertion reuccatpfxs1v
|- ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x prefix ( # ` W ) ) ) )

Proof

Step Hyp Ref Expression
1 nfcv
 |-  F/_ v X
2 1 reuccatpfxs1
 |-  ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x prefix ( # ` W ) ) ) )