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

Proof

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