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 ⊢ x = ∅ ∧ w = ∅ → φ ↔ ψ
wrd2ind.2 ⊢ x = y ∧ w = u → φ ↔ χ
wrd2ind.3 ⊢ x = y ++ ⟨“ z ”⟩ ∧ w = u ++ ⟨“ s ”⟩ → φ ↔ θ
wrd2ind.4 ⊢ x = A → ρ ↔ τ
wrd2ind.5 ⊢ w = B → φ ↔ ρ
wrd2ind.6 ⊢ ψ
wrd2ind.7 ⊢ y ∈ Word X ∧ z ∈ X ∧ u ∈ Word Y ∧ s ∈ Y ∧ y = u → χ → θ
Assertion wrd2ind ⊢ A ∈ Word X ∧ B ∈ Word Y ∧ A = B → τ

Proof

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