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 ∈ Word V ∧ ∀ x ∈ X x ∈ Word V ∧ x = W + 1 → ∃! v ∈ V W ++ ⟨“ v ”⟩ ∈ X → ∃! x ∈ X W = x prefix W

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ v X
2 1 reuccatpfxs1 ⊢ W ∈ Word V ∧ ∀ x ∈ X x ∈ Word V ∧ x = W + 1 → ∃! v ∈ V W ++ ⟨“ v ”⟩ ∈ X → ∃! x ∈ X W = x prefix W