Metamath Proof Explorer

Theorem wrdind

Description: Perform induction over the structure of a word. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 26-Feb-2016) (Proof shortened by AV, 12-Oct-2022)

Ref Expression
Hypotheses wrdind.1 ⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
wrdind.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
wrdind.3 ⊢ ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( 𝜑 ↔ 𝜃 ) )
wrdind.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
wrdind.5 ⊢ 𝜓
wrdind.6 ⊢ ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝜒 → 𝜃 ) )
Assertion wrdind ( 𝐴 ∈ Word 𝐵 → 𝜏 )

Proof

Step Hyp Ref Expression
1 wrdind.1 ⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
2 wrdind.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 wrdind.3 ⊢ ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( 𝜑 ↔ 𝜃 ) )
4 wrdind.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5 wrdind.5 ⊢ 𝜓
6 wrdind.6 ⊢ ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝜒 → 𝜃 ) )
7 lencl ⊢ ( 𝐴 ∈ Word 𝐵 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
8 eqeq2 ⊢ ( 𝑛 = 0 → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = 0 ) )
9 8 imbi1d ⊢ ( 𝑛 = 0 → ( ( ( ♯ ‘ 𝑥 ) = 𝑛 → 𝜑 ) ↔ ( ( ♯ ‘ 𝑥 ) = 0 → 𝜑 ) ) )
10 9 ralbidv ⊢ ( 𝑛 = 0 → ( ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 𝑛 → 𝜑 ) ↔ ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 0 → 𝜑 ) ) )
11 eqeq2 ⊢ ( 𝑛 = 𝑚 → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = 𝑚 ) )
12 11 imbi1d ⊢ ( 𝑛 = 𝑚 → ( ( ( ♯ ‘ 𝑥 ) = 𝑛 → 𝜑 ) ↔ ( ( ♯ ‘ 𝑥 ) = 𝑚 → 𝜑 ) ) )
13 12 ralbidv ⊢ ( 𝑛 = 𝑚 → ( ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 𝑛 → 𝜑 ) ↔ ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 𝑚 → 𝜑 ) ) )
14 eqeq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) )
15 14 imbi1d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( ♯ ‘ 𝑥 ) = 𝑛 → 𝜑 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → 𝜑 ) ) )
16 15 ralbidv ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 𝑛 → 𝜑 ) ↔ ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → 𝜑 ) ) )
17 eqeq2 ⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) )
18 17 imbi1d ⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( ( ♯ ‘ 𝑥 ) = 𝑛 → 𝜑 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) → 𝜑 ) ) )
19 18 ralbidv ⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 𝑛 → 𝜑 ) ↔ ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) → 𝜑 ) ) )
20 hasheq0 ⊢ ( 𝑥 ∈ Word 𝐵 → ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ ) )
21 5 1 mpbiri ⊢ ( 𝑥 = ∅ → 𝜑 )
22 20 21 syl6bi ⊢ ( 𝑥 ∈ Word 𝐵 → ( ( ♯ ‘ 𝑥 ) = 0 → 𝜑 ) )
23 22 rgen ⊢ ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 0 → 𝜑 )
24 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) = 𝑚 ↔ ( ♯ ‘ 𝑦 ) = 𝑚 ) )
25 24 2 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( ♯ ‘ 𝑥 ) = 𝑚 → 𝜑 ) ↔ ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) )
26 25 cbvralvw ⊢ ( ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 𝑚 → 𝜑 ) ↔ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) )
27 simprl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → 𝑥 ∈ Word 𝐵 )
28 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑥 ) )
29 simprr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) )
30 nn0p1nn ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ )
31 30 ad2antrr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( 𝑚 + 1 ) ∈ ℕ )
32 29 31 eqeltrd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ )
33 fzo0end ⊢ ( ( ♯ ‘ 𝑥 ) ∈ ℕ → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) )
34 32 33 syl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) )
35 28 34 sselid ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
36 pfxlen ⊢ ( ( 𝑥 ∈ Word 𝐵 ∧ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑥 ) − 1 ) )
37 27 35 36 syl2anc ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑥 ) − 1 ) )
38 29 oveq1d ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) = ( ( 𝑚 + 1 ) − 1 ) )
39 nn0cn ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℂ )
40 39 ad2antrr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → 𝑚 ∈ ℂ )
41 ax-1cn ⊢ 1 ∈ ℂ
42 pncan ⊢ ( ( 𝑚 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
43 40 41 42 sylancl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
44 37 38 43 3eqtrd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 )
45 fveqeq2 ⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = 𝑚 ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) )
46 vex ⊢ 𝑦 ∈ V
47 46 2 sbcie ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜒 )
48 dfsbcq ⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 ) )
49 47 48 bitr3id ⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( 𝜒 ↔ [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 ) )
50 45 49 imbi12d ⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ↔ ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 ) ) )
51 simplr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) )
52 pfxcl ⊢ ( 𝑥 ∈ Word 𝐵 → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝐵 )
53 52 ad2antrl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝐵 )
54 50 51 53 rspcdva ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 ) )
55 44 54 mpd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 )
56 32 nnge1d ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → 1 ≤ ( ♯ ‘ 𝑥 ) )
57 wrdlenge1n0 ⊢ ( 𝑥 ∈ Word 𝐵 → ( 𝑥 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑥 ) ) )
58 57 ad2antrl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( 𝑥 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑥 ) ) )
59 56 58 mpbird ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → 𝑥 ≠ ∅ )
60 lswcl ⊢ ( ( 𝑥 ∈ Word 𝐵 ∧ 𝑥 ≠ ∅ ) → ( lastS ‘ 𝑥 ) ∈ 𝐵 )
61 27 59 60 syl2anc ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( lastS ‘ 𝑥 ) ∈ 𝐵 )
62 oveq1 ⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) )
63 62 sbceq1d ⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) )
64 48 63 imbi12d ⊢ ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( [ 𝑦 / 𝑥 ] 𝜑 → [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ↔ ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ) )
65 s1eq ⊢ ( 𝑧 = ( lastS ‘ 𝑥 ) → ⟨“ 𝑧 ”⟩ = ⟨“ ( lastS ‘ 𝑥 ) ”⟩ )
66 65 oveq2d ⊢ ( 𝑧 = ( lastS ‘ 𝑥 ) → ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) )
67 66 sbceq1d ⊢ ( 𝑧 = ( lastS ‘ 𝑥 ) → ( [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] 𝜑 ) )
68 67 imbi2d ⊢ ( 𝑧 = ( lastS ‘ 𝑥 ) → ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ↔ ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] 𝜑 ) ) )
69 ovex ⊢ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ∈ V
70 69 3 sbcie ⊢ ( [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ↔ 𝜃 )
71 6 47 70 3imtr4g ⊢ ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) )
72 64 68 71 vtocl2ga ⊢ ( ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝐵 ∧ ( lastS ‘ 𝑥 ) ∈ 𝐵 ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] 𝜑 ) )
73 53 61 72 syl2anc ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] 𝜑 → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] 𝜑 ) )
74 55 73 mpd ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] 𝜑 )
75 wrdfin ⊢ ( 𝑥 ∈ Word 𝐵 → 𝑥 ∈ Fin )
76 75 ad2antrl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → 𝑥 ∈ Fin )
77 hashnncl ⊢ ( 𝑥 ∈ Fin → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ 𝑥 ≠ ∅ ) )
78 76 77 syl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ 𝑥 ≠ ∅ ) )
79 32 78 mpbid ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → 𝑥 ≠ ∅ )
80 pfxlswccat ⊢ ( ( 𝑥 ∈ Word 𝐵 ∧ 𝑥 ≠ ∅ ) → ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) = 𝑥 )
81 80 eqcomd ⊢ ( ( 𝑥 ∈ Word 𝐵 ∧ 𝑥 ≠ ∅ ) → 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) )
82 27 79 81 syl2anc ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) )
83 sbceq1a ⊢ ( 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) → ( 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] 𝜑 ) )
84 82 83 syl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( 𝜑 ↔ [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] 𝜑 ) )
85 74 84 mpbird ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ ( 𝑥 ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → 𝜑 )
86 85 expr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) ∧ 𝑥 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → 𝜑 ) )
87 86 ralrimiva ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) ) → ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → 𝜑 ) )
88 87 ex ⊢ ( 𝑚 ∈ ℕ0 → ( ∀ 𝑦 ∈ Word 𝐵 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝜒 ) → ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → 𝜑 ) ) )
89 26 88 syl5bi ⊢ ( 𝑚 ∈ ℕ0 → ( ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = 𝑚 → 𝜑 ) → ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → 𝜑 ) ) )
90 10 13 16 19 23 89 nn0ind ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) → 𝜑 ) )
91 7 90 syl ⊢ ( 𝐴 ∈ Word 𝐵 → ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) → 𝜑 ) )
92 eqidd ⊢ ( 𝐴 ∈ Word 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) )
93 fveqeq2 ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) )
94 93 4 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) → 𝜑 ) ↔ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → 𝜏 ) ) )
95 94 rspcv ⊢ ( 𝐴 ∈ Word 𝐵 → ( ∀ 𝑥 ∈ Word 𝐵 ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) → 𝜑 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → 𝜏 ) ) )
96 91 92 95 mp2d ⊢ ( 𝐴 ∈ Word 𝐵 → 𝜏 )