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 \in Word V \land \forall x \in X (x \in Word V \land \|x\| = \|W\| + 1)) \to (\exists! v \in V W ++ ⟨“ v ”⟩ \in X \to \exists! x \in X W = x prefix \|W\|)$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$⊢ \underline{Ⅎ} v X$
2	1	reuccatpfxs1	$⊢ (W \in Word V \land \forall x \in X (x \in Word V \land \|x\| = \|W\| + 1)) \to (\exists! v \in V W ++ ⟨“ v ”⟩ \in X \to \exists! x \in X W = x prefix \|W\|)$