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

Metamath Proof Explorer

Theorem reuccatpfxs1

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, 13-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 reuccatpfxs1.1 ⊢ Ⅎ 𝑣 𝑋
2 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ Word 𝑉 ↔ 𝑦 ∈ Word 𝑉 ) )
3 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ↔ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
4 2 3 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ↔ ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) )
5 4 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
6 1 nfel2 ⊢ Ⅎ 𝑣 ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋
7 1 nfel2 ⊢ Ⅎ 𝑣 ( 𝑊 ++ ⟨“ 𝑥 ”⟩ ) ∈ 𝑋
8 s1eq ⊢ ( 𝑣 = 𝑥 → ⟨“ 𝑣 ”⟩ = ⟨“ 𝑥 ”⟩ )
9 8 oveq2d ⊢ ( 𝑣 = 𝑥 → ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑥 ”⟩ ) )
10 9 eleq1d ⊢ ( 𝑣 = 𝑥 → ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ↔ ( 𝑊 ++ ⟨“ 𝑥 ”⟩ ) ∈ 𝑋 ) )
11 s1eq ⊢ ( 𝑥 = 𝑢 → ⟨“ 𝑥 ”⟩ = ⟨“ 𝑢 ”⟩ )
12 11 oveq2d ⊢ ( 𝑥 = 𝑢 → ( 𝑊 ++ ⟨“ 𝑥 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) )
13 12 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑊 ++ ⟨“ 𝑥 ”⟩ ) ∈ 𝑋 ↔ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) )
14 6 7 10 13 reu8nf ⊢ ( ∃! 𝑣 ∈ 𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ↔ ∃ 𝑣 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) )
15 nfv ⊢ Ⅎ 𝑣 𝑊 ∈ Word 𝑉
16 nfv ⊢ Ⅎ 𝑣 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
17 1 16 nfralw ⊢ Ⅎ 𝑣 ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
18 15 17 nfan ⊢ Ⅎ 𝑣 ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
19 nfv ⊢ Ⅎ 𝑣 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) )
20 1 19 nfreuw ⊢ Ⅎ 𝑣 ∃! 𝑥 ∈ 𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) )
21 simprl ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) → ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 )
22 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → 𝑊 ∈ Word 𝑉 )
23 22 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) → 𝑊 ∈ Word 𝑉 )
24 23 anim1i ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑊 ∈ Word 𝑉 ∧ 𝑥 ∈ 𝑋 ) )
25 simplrr ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) )
26 simp-4r ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
27 reuccatpfxs1lem ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑥 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) → 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ) )
28 24 25 26 27 syl3anc ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) → 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ) )
29 oveq1 ⊢ ( 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) → ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) = ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) )
30 s1cl ⊢ ( 𝑣 ∈ 𝑉 → ⟨“ 𝑣 ”⟩ ∈ Word 𝑉 )
31 22 30 anim12i ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑣 ”⟩ ∈ Word 𝑉 ) )
32 31 ad2antrr ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑣 ”⟩ ∈ Word 𝑉 ) )
33 pfxccat1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑣 ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
34 32 33 syl ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
35 29 34 sylan9eqr ⊢ ( ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ) → ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
36 35 eqcomd ⊢ ( ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ) → 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) )
37 36 ex ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) → 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ) )
38 28 37 impbid ⊢ ( ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ↔ 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ) )
39 38 ralrimiva ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ↔ 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ) )
40 reu6i ⊢ ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ↔ 𝑥 = ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ) ) → ∃! 𝑥 ∈ 𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) )
41 21 39 40 syl2anc ⊢ ( ( ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) ) → ∃! 𝑥 ∈ 𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) )
42 41 exp31 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑣 ∈ 𝑉 → ( ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) → ∃! 𝑥 ∈ 𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ) ) )
43 18 20 42 rexlimd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∃ 𝑣 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝑉 ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → 𝑣 = 𝑢 ) ) → ∃! 𝑥 ∈ 𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ) )
44 14 43 biimtrid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∃! 𝑣 ∈ 𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 → ∃! 𝑥 ∈ 𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ) )
45 5 44 sylan2b ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∃! 𝑣 ∈ 𝑉 ( 𝑊 ++ ⟨“ 𝑣 ”⟩ ) ∈ 𝑋 → ∃! 𝑥 ∈ 𝑋 𝑊 = ( 𝑥 prefix ( ♯ ‘ 𝑊 ) ) ) )