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 ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑥𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∃! 𝑣𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 → ∃! 𝑥𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 nfcv 𝑣 𝑋
2 1 reuccatpfxs1 ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑥𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∃! 𝑣𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 → ∃! 𝑥𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ) )