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

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 ) ) ) )