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 sseldi ⊢ ( ( ( 𝑚 ∈ ℕ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 𝑌 ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) → 𝜏 )