Metamath Proof Explorer


Theorem wrd2ind

Description: Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019) (Proof shortened by AV, 12-Oct-2022)

Ref Expression
Hypotheses wrd2ind.1 ( ( 𝑥 = ∅ ∧ 𝑤 = ∅ ) → ( 𝜑𝜓 ) )
wrd2ind.2 ( ( 𝑥 = 𝑦𝑤 = 𝑢 ) → ( 𝜑𝜒 ) )
wrd2ind.3 ( ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ∧ 𝑤 = ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) ) → ( 𝜑𝜃 ) )
wrd2ind.4 ( 𝑥 = 𝐴 → ( 𝜌𝜏 ) )
wrd2ind.5 ( 𝑤 = 𝐵 → ( 𝜑𝜌 ) )
wrd2ind.6 𝜓
wrd2ind.7 ( ( ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ∧ ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝜒𝜃 ) )
Assertion wrd2ind ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 wrd2ind.1 ( ( 𝑥 = ∅ ∧ 𝑤 = ∅ ) → ( 𝜑𝜓 ) )
2 wrd2ind.2 ( ( 𝑥 = 𝑦𝑤 = 𝑢 ) → ( 𝜑𝜒 ) )
3 wrd2ind.3 ( ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ∧ 𝑤 = ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) ) → ( 𝜑𝜃 ) )
4 wrd2ind.4 ( 𝑥 = 𝐴 → ( 𝜌𝜏 ) )
5 wrd2ind.5 ( 𝑤 = 𝐵 → ( 𝜑𝜌 ) )
6 wrd2ind.6 𝜓
7 wrd2ind.7 ( ( ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ∧ ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝜒𝜃 ) )
8 lencl ( 𝐴 ∈ Word 𝑋 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
9 eqeq2 ( 𝑛 = 0 → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = 0 ) )
10 9 anbi2d ( 𝑛 = 0 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) ) )
11 10 imbi1d ( 𝑛 = 0 → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → 𝜑 ) ) )
12 11 2ralbidv ( 𝑛 = 0 → ( ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → 𝜑 ) ) )
13 eqeq2 ( 𝑛 = 𝑚 → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = 𝑚 ) )
14 13 anbi2d ( 𝑛 = 𝑚 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) ) )
15 14 imbi1d ( 𝑛 = 𝑚 → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ) )
16 15 2ralbidv ( 𝑛 = 𝑚 → ( ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ) )
17 eqeq2 ( 𝑛 = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) )
18 17 anbi2d ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) )
19 18 imbi1d ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) )
20 19 2ralbidv ( 𝑛 = ( 𝑚 + 1 ) → ( ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) )
21 eqeq2 ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) )
22 21 anbi2d ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ) )
23 22 imbi1d ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ) )
24 23 2ralbidv ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) → 𝜑 ) ↔ ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ) )
25 eqeq1 ( ( ♯ ‘ 𝑥 ) = 0 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ 0 = ( ♯ ‘ 𝑤 ) ) )
26 25 adantl ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ 0 = ( ♯ ‘ 𝑤 ) ) )
27 eqcom ( 0 = ( ♯ ‘ 𝑤 ) ↔ ( ♯ ‘ 𝑤 ) = 0 )
28 hasheq0 ( 𝑤 ∈ Word 𝑌 → ( ( ♯ ‘ 𝑤 ) = 0 ↔ 𝑤 = ∅ ) )
29 27 28 syl5bb ( 𝑤 ∈ Word 𝑌 → ( 0 = ( ♯ ‘ 𝑤 ) ↔ 𝑤 = ∅ ) )
30 hasheq0 ( 𝑥 ∈ Word 𝑋 → ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ ) )
31 6 1 mpbiri ( ( 𝑥 = ∅ ∧ 𝑤 = ∅ ) → 𝜑 )
32 31 ex ( 𝑥 = ∅ → ( 𝑤 = ∅ → 𝜑 ) )
33 30 32 syl6bi ( 𝑥 ∈ Word 𝑋 → ( ( ♯ ‘ 𝑥 ) = 0 → ( 𝑤 = ∅ → 𝜑 ) ) )
34 33 com13 ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑥 ) = 0 → ( 𝑥 ∈ Word 𝑋𝜑 ) ) )
35 29 34 syl6bi ( 𝑤 ∈ Word 𝑌 → ( 0 = ( ♯ ‘ 𝑤 ) → ( ( ♯ ‘ 𝑥 ) = 0 → ( 𝑥 ∈ Word 𝑋𝜑 ) ) ) )
36 35 com24 ( 𝑤 ∈ Word 𝑌 → ( 𝑥 ∈ Word 𝑋 → ( ( ♯ ‘ 𝑥 ) = 0 → ( 0 = ( ♯ ‘ 𝑤 ) → 𝜑 ) ) ) )
37 36 imp31 ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → ( 0 = ( ♯ ‘ 𝑤 ) → 𝜑 ) )
38 26 37 sylbid ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) → 𝜑 ) )
39 38 ex ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) → ( ( ♯ ‘ 𝑥 ) = 0 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) → 𝜑 ) ) )
40 39 impcomd ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → 𝜑 ) )
41 40 rgen2 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 0 ) → 𝜑 )
42 fveq2 ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
43 fveq2 ( 𝑤 = 𝑢 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑢 ) )
44 42 43 eqeqan12d ( ( 𝑥 = 𝑦𝑤 = 𝑢 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) )
45 fveqeq2 ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) = 𝑚 ↔ ( ♯ ‘ 𝑦 ) = 𝑚 ) )
46 45 adantr ( ( 𝑥 = 𝑦𝑤 = 𝑢 ) → ( ( ♯ ‘ 𝑥 ) = 𝑚 ↔ ( ♯ ‘ 𝑦 ) = 𝑚 ) )
47 44 46 anbi12d ( ( 𝑥 = 𝑦𝑤 = 𝑢 ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) ↔ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) )
48 47 2 imbi12d ( ( 𝑥 = 𝑦𝑤 = 𝑢 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) )
49 48 ancoms ( ( 𝑤 = 𝑢𝑥 = 𝑦 ) → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) )
50 49 cbvraldva ( 𝑤 = 𝑢 → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ↔ ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) )
51 50 cbvralvw ( ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) ↔ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) )
52 pfxcl ( 𝑤 ∈ Word 𝑌 → ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 )
53 52 adantr ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) → ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 )
54 53 ad2antrl ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 )
55 simprll ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ∈ Word 𝑌 )
56 eqeq1 ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ ( 𝑚 + 1 ) = ( ♯ ‘ 𝑤 ) ) )
57 nn0p1nn ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ )
58 eleq1 ( ( ♯ ‘ 𝑤 ) = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ ( 𝑚 + 1 ) ∈ ℕ ) )
59 58 eqcoms ( ( 𝑚 + 1 ) = ( ♯ ‘ 𝑤 ) → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ ( 𝑚 + 1 ) ∈ ℕ ) )
60 57 59 syl5ibr ( ( 𝑚 + 1 ) = ( ♯ ‘ 𝑤 ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑤 ) ∈ ℕ ) )
61 56 60 syl6bi ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑤 ) ∈ ℕ ) ) )
62 61 impcom ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑤 ) ∈ ℕ ) )
63 62 adantl ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑤 ) ∈ ℕ ) )
64 63 impcom ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
65 64 nnge1d ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 1 ≤ ( ♯ ‘ 𝑤 ) )
66 wrdlenge1n0 ( 𝑤 ∈ Word 𝑌 → ( 𝑤 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑤 ) ) )
67 55 66 syl ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑤 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑤 ) ) )
68 65 67 mpbird ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ≠ ∅ )
69 lswcl ( ( 𝑤 ∈ Word 𝑌𝑤 ≠ ∅ ) → ( lastS ‘ 𝑤 ) ∈ 𝑌 )
70 55 68 69 syl2anc ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( lastS ‘ 𝑤 ) ∈ 𝑌 )
71 54 70 jca ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑌 ) )
72 pfxcl ( 𝑥 ∈ Word 𝑋 → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 )
73 72 adantl ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 )
74 73 ad2antrl ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 )
75 simprlr ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ∈ Word 𝑋 )
76 eleq1 ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ ( 𝑚 + 1 ) ∈ ℕ ) )
77 57 76 syl5ibr ( ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑥 ) ∈ ℕ ) )
78 77 ad2antll ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) → ( 𝑚 ∈ ℕ0 → ( ♯ ‘ 𝑥 ) ∈ ℕ ) )
79 78 impcom ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ )
80 79 nnge1d ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 1 ≤ ( ♯ ‘ 𝑥 ) )
81 wrdlenge1n0 ( 𝑥 ∈ Word 𝑋 → ( 𝑥 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑥 ) ) )
82 75 81 syl ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑥 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑥 ) ) )
83 80 82 mpbird ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ≠ ∅ )
84 lswcl ( ( 𝑥 ∈ Word 𝑋𝑥 ≠ ∅ ) → ( lastS ‘ 𝑥 ) ∈ 𝑋 )
85 75 83 84 syl2anc ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( lastS ‘ 𝑥 ) ∈ 𝑋 )
86 71 74 85 jca32 ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑌 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ∧ ( lastS ‘ 𝑥 ) ∈ 𝑋 ) ) )
87 86 adantlr ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑌 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ∧ ( lastS ‘ 𝑥 ) ∈ 𝑋 ) ) )
88 simprl ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) )
89 simplr ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) )
90 simprrl ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) )
91 90 oveq1d ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) = ( ( ♯ ‘ 𝑤 ) − 1 ) )
92 simprlr ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ∈ Word 𝑋 )
93 fzossfz ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑥 ) )
94 simprrr ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) )
95 57 ad2antrr ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝑚 + 1 ) ∈ ℕ )
96 94 95 eqeltrd ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ )
97 fzo0end ( ( ♯ ‘ 𝑥 ) ∈ ℕ → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) )
98 96 97 syl ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) )
99 93 98 sselid ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
100 pfxlen ( ( 𝑥 ∈ Word 𝑋 ∧ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑥 ) − 1 ) )
101 92 99 100 syl2anc ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑥 ) − 1 ) )
102 simprll ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ∈ Word 𝑌 )
103 oveq1 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( ( ♯ ‘ 𝑥 ) − 1 ) )
104 oveq2 ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) → ( 0 ... ( ♯ ‘ 𝑤 ) ) = ( 0 ... ( ♯ ‘ 𝑥 ) ) )
105 103 104 eleq12d ( ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
106 105 eqcoms ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
107 106 adantr ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
108 107 ad2antll ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↔ ( ( ♯ ‘ 𝑥 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
109 99 108 mpbird ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) )
110 pfxlen ( ( 𝑤 ∈ Word 𝑌 ∧ ( ( ♯ ‘ 𝑤 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑤 ) − 1 ) )
111 102 109 110 syl2anc ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑤 ) − 1 ) )
112 91 101 111 3eqtr4d ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) )
113 94 oveq1d ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) − 1 ) = ( ( 𝑚 + 1 ) − 1 ) )
114 nn0cn ( 𝑚 ∈ ℕ0𝑚 ∈ ℂ )
115 114 ad2antrr ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑚 ∈ ℂ )
116 ax-1cn 1 ∈ ℂ
117 pncan ( ( 𝑚 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
118 115 116 117 sylancl ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
119 101 113 118 3eqtrd ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 )
120 112 119 jca ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) )
121 73 adantr ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 )
122 fveq2 ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) )
123 fveq2 ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) )
124 122 123 eqeqan12d ( ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )
125 124 expcom ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) )
126 125 adantl ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) )
127 126 imp ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )
128 fveqeq2 ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = 𝑚 ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) )
129 128 adantl ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑦 ) = 𝑚 ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) )
130 127 129 anbi12d ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ↔ ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) ) )
131 vex 𝑦 ∈ V
132 vex 𝑢 ∈ V
133 131 132 2 sbc2ie ( [ 𝑦 / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑𝜒 )
134 133 bicomi ( 𝜒[ 𝑦 / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 )
135 134 a1i ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( 𝜒[ 𝑦 / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ) )
136 simpr ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
137 136 sbceq1d ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( [ 𝑦 / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑[ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑 ) )
138 dfsbcq ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ 𝑢 / 𝑤 ] 𝜑[ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) )
139 138 sbcbidv ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑[ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) )
140 139 adantl ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑[ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) )
141 140 adantr ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ 𝑢 / 𝑤 ] 𝜑[ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) )
142 135 137 141 3bitrd ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( 𝜒[ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) )
143 130 142 imbi12d ( ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) → ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ↔ ( ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) )
144 121 143 rspcdv ( ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) → ( ∀ 𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) → ( ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) )
145 53 144 rspcimdv ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) → ( ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) → ( ( ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = 𝑚 ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) ) )
146 88 89 120 145 syl3c ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 )
147 146 112 jca ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )
148 dfsbcq ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑[ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
149 sbccom ( [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑[ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 )
150 148 149 bitrdi ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑[ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) )
151 123 eqeq2d ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ↔ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )
152 150 151 anbi12d ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) ↔ ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) )
153 oveq1 ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ 𝑠 ”⟩ ) )
154 153 sbceq1d ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( [ ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑[ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) )
155 152 154 imbi12d ( 𝑢 = ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) → ( ( ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → [ ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ↔ ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ) )
156 s1eq ( 𝑠 = ( lastS ‘ 𝑤 ) → ⟨“ 𝑠 ”⟩ = ⟨“ ( lastS ‘ 𝑤 ) ”⟩ )
157 156 oveq2d ( 𝑠 = ( lastS ‘ 𝑤 ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ 𝑠 ”⟩ ) = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
158 157 sbceq1d ( 𝑠 = ( lastS ‘ 𝑤 ) → ( [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑[ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) )
159 158 imbi2d ( 𝑠 = ( lastS ‘ 𝑤 ) → ( ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ↔ ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ) )
160 sbccom ( [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑[ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 )
161 160 a1i ( 𝑠 = ( lastS ‘ 𝑤 ) → ( [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑[ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) )
162 161 imbi2d ( 𝑠 = ( lastS ‘ 𝑤 ) → ( ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ↔ ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) ) )
163 159 162 bitrd ( 𝑠 = ( lastS ‘ 𝑤 ) → ( ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ↔ ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) ) )
164 dfsbcq ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑[ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ) )
165 fveqeq2 ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ↔ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) )
166 164 165 anbi12d ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ↔ ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) ) )
167 oveq1 ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) )
168 167 sbceq1d ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑[ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) )
169 166 168 imbi12d ( 𝑦 = ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) → ( ( ( [ 𝑦 / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) ↔ ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) ) )
170 s1eq ( 𝑧 = ( lastS ‘ 𝑥 ) → ⟨“ 𝑧 ”⟩ = ⟨“ ( lastS ‘ 𝑥 ) ”⟩ )
171 170 oveq2d ( 𝑧 = ( lastS ‘ 𝑥 ) → ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) )
172 171 sbceq1d ( 𝑧 = ( lastS ‘ 𝑥 ) → ( [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑[ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) )
173 172 imbi2d ( 𝑧 = ( lastS ‘ 𝑥 ) → ( ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) ↔ ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) ) )
174 simplr ( ( ( ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) )
175 simpll ( ( ( ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) )
176 simpr ( ( ( ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) )
177 174 175 176 7 syl3anc ( ( ( ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( 𝜒𝜃 ) )
178 2 ancoms ( ( 𝑤 = 𝑢𝑥 = 𝑦 ) → ( 𝜑𝜒 ) )
179 132 131 178 sbc2ie ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑𝜒 )
180 ovex ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) ∈ V
181 ovex ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ∈ V
182 3 ancoms ( ( 𝑤 = ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) ∧ 𝑥 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) → ( 𝜑𝜃 ) )
183 180 181 182 sbc2ie ( [ ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑𝜃 )
184 177 179 183 3imtr4g ( ( ( ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ) ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑[ ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) )
185 184 ex ( ( ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) → ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑[ ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) ) )
186 185 impcomd ( ( ( 𝑢 ∈ Word 𝑌𝑠𝑌 ) ∧ ( 𝑦 ∈ Word 𝑋𝑧𝑋 ) ) → ( ( [ 𝑢 / 𝑤 ] [ 𝑦 / 𝑥 ] 𝜑 ∧ ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ) → [ ( 𝑢 ++ ⟨“ 𝑠 ”⟩ ) / 𝑤 ] [ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) / 𝑥 ] 𝜑 ) )
187 155 163 169 173 186 vtocl4ga ( ( ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ∈ Word 𝑌 ∧ ( lastS ‘ 𝑤 ) ∈ 𝑌 ) ∧ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ Word 𝑋 ∧ ( lastS ‘ 𝑥 ) ∈ 𝑋 ) ) → ( ( [ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) / 𝑥 ] [ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) / 𝑤 ] 𝜑 ∧ ( ♯ ‘ ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ) = ( ♯ ‘ ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) )
188 87 147 187 sylc ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → [ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 )
189 eqtr2 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → ( ♯ ‘ 𝑤 ) = ( 𝑚 + 1 ) )
190 189 ad2antll ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑤 ) = ( 𝑚 + 1 ) )
191 190 95 eqeltrd ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ♯ ‘ 𝑤 ) ∈ ℕ )
192 wrdfin ( 𝑤 ∈ Word 𝑌𝑤 ∈ Fin )
193 192 adantr ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) → 𝑤 ∈ Fin )
194 193 ad2antrl ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ∈ Fin )
195 hashnncl ( 𝑤 ∈ Fin → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ 𝑤 ≠ ∅ ) )
196 194 195 syl ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑤 ) ∈ ℕ ↔ 𝑤 ≠ ∅ ) )
197 191 196 mpbid ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 ≠ ∅ )
198 pfxlswccat ( ( 𝑤 ∈ Word 𝑌𝑤 ≠ ∅ ) → ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) = 𝑤 )
199 198 eqcomd ( ( 𝑤 ∈ Word 𝑌𝑤 ≠ ∅ ) → 𝑤 = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
200 102 197 199 syl2anc ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑤 = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) )
201 wrdfin ( 𝑥 ∈ Word 𝑋𝑥 ∈ Fin )
202 201 adantl ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) → 𝑥 ∈ Fin )
203 202 ad2antrl ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ∈ Fin )
204 hashnncl ( 𝑥 ∈ Fin → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ 𝑥 ≠ ∅ ) )
205 203 204 syl ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ 𝑥 ≠ ∅ ) )
206 96 205 mpbid ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 ≠ ∅ )
207 pfxlswccat ( ( 𝑥 ∈ Word 𝑋𝑥 ≠ ∅ ) → ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) = 𝑥 )
208 207 eqcomd ( ( 𝑥 ∈ Word 𝑋𝑥 ≠ ∅ ) → 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) )
209 92 206 208 syl2anc ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) )
210 sbceq1a ( 𝑤 = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) → ( 𝜑[ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) )
211 sbceq1a ( 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) → ( [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑[ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) )
212 210 211 sylan9bb ( ( 𝑤 = ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) ∧ 𝑥 = ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) ) → ( 𝜑[ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) )
213 200 209 212 syl2anc ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → ( 𝜑[ ( ( 𝑥 prefix ( ( ♯ ‘ 𝑥 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑥 ) ”⟩ ) / 𝑥 ] [ ( ( 𝑤 prefix ( ( ♯ ‘ 𝑤 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑤 ) ”⟩ ) / 𝑤 ] 𝜑 ) )
214 188 213 mpbird ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ∧ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) ) ) → 𝜑 )
215 214 expr ( ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) ∧ ( 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ) ) → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) )
216 215 ralrimivva ( ( 𝑚 ∈ ℕ0 ∧ ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) ) → ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) )
217 216 ex ( 𝑚 ∈ ℕ0 → ( ∀ 𝑢 ∈ Word 𝑌𝑦 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑢 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → 𝜒 ) → ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) )
218 51 217 syl5bi ( 𝑚 ∈ ℕ0 → ( ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑚 ) → 𝜑 ) → ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( 𝑚 + 1 ) ) → 𝜑 ) ) )
219 12 16 20 24 41 218 nn0ind ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) )
220 8 219 syl ( 𝐴 ∈ Word 𝑋 → ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) )
221 220 3ad2ant1 ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) )
222 fveq2 ( 𝑤 = 𝐵 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝐵 ) )
223 222 eqeq2d ( 𝑤 = 𝐵 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ↔ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) )
224 223 anbi1d ( 𝑤 = 𝐵 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ) )
225 224 5 imbi12d ( 𝑤 = 𝐵 → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ↔ ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) )
226 225 ralbidv ( 𝑤 = 𝐵 → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) ↔ ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) )
227 226 rspcv ( 𝐵 ∈ Word 𝑌 → ( ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) → ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) )
228 227 3ad2ant2 ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( ∀ 𝑤 ∈ Word 𝑌𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜑 ) → ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ) )
229 221 228 mpd ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) )
230 eqidd ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) )
231 fveqeq2 ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
232 fveqeq2 ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) )
233 231 232 anbi12d ( 𝑥 = 𝐴 → ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) ↔ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) ) )
234 233 4 imbi12d ( 𝑥 = 𝐴 → ( ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) ↔ ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) → 𝜏 ) ) )
235 234 rspcv ( 𝐴 ∈ Word 𝑋 → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) → 𝜏 ) ) )
236 235 com23 ( 𝐴 ∈ Word 𝑋 → ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → 𝜏 ) ) )
237 236 expd ( 𝐴 ∈ Word 𝑋 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → 𝜏 ) ) ) )
238 237 com34 ( 𝐴 ∈ Word 𝑋 → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → 𝜏 ) ) ) )
239 238 imp ( ( 𝐴 ∈ Word 𝑋 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → 𝜏 ) ) )
240 239 3adant2 ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → ( ∀ 𝑥 ∈ Word 𝑋 ( ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) ) → 𝜌 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) → 𝜏 ) ) )
241 229 230 240 mp2d ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → 𝜏 )