Metamath Proof Explorer

Theorem chnerlem1

Description: In a chain constructed on an equivalence relation, the last element is equivalent to any. This theorem is a translation of chnub to equivalence relations. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses chner.1 ⊢ ( 𝜑 → ∼ Er 𝐴 )
chner.2 ⊢ ( 𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴 ) )
chner.3 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
Assertion chnerlem1 ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∼ ( lastS ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 chner.1 ⊢ ( 𝜑 → ∼ Er 𝐴 )
2 chner.2 ⊢ ( 𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴 ) )
3 chner.3 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
4 fveq2 ⊢ ( 𝑖 = 𝐽 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝐽 ) )
5 4 breq1d ⊢ ( 𝑖 = 𝐽 → ( ( 𝐶 ‘ 𝑖 ) ∼ ( lastS ‘ 𝐶 ) ↔ ( 𝐶 ‘ 𝐽 ) ∼ ( lastS ‘ 𝐶 ) ) )
6 fveq2 ⊢ ( 𝑐 = ∅ → ( ♯ ‘ 𝑐 ) = ( ♯ ‘ ∅ ) )
7 6 oveq2d ⊢ ( 𝑐 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑐 ) ) = ( 0 ..^ ( ♯ ‘ ∅ ) ) )
8 fveq1 ⊢ ( 𝑐 = ∅ → ( 𝑐 ‘ 𝑖 ) = ( ∅ ‘ 𝑖 ) )
9 fveq2 ⊢ ( 𝑐 = ∅ → ( lastS ‘ 𝑐 ) = ( lastS ‘ ∅ ) )
10 8 9 breq12d ⊢ ( 𝑐 = ∅ → ( ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ( ∅ ‘ 𝑖 ) ∼ ( lastS ‘ ∅ ) ) )
11 7 10 raleqbidv ⊢ ( 𝑐 = ∅ → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑐 ) ) ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∼ ( lastS ‘ ∅ ) ) )
12 fveq2 ⊢ ( 𝑐 = 𝑑 → ( ♯ ‘ 𝑐 ) = ( ♯ ‘ 𝑑 ) )
13 12 oveq2d ⊢ ( 𝑐 = 𝑑 → ( 0 ..^ ( ♯ ‘ 𝑐 ) ) = ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
14 fveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
15 fveq2 ⊢ ( 𝑐 = 𝑑 → ( lastS ‘ 𝑐 ) = ( lastS ‘ 𝑑 ) )
16 14 15 breq12d ⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) )
17 13 16 raleqbidv ⊢ ( 𝑐 = 𝑑 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑐 ) ) ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) )
18 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑗 ) )
19 18 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ( 𝑐 ‘ 𝑗 ) ∼ ( lastS ‘ 𝑐 ) ) )
20 19 cbvralvw ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑐 ) ) ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑐 ) ) ( 𝑐 ‘ 𝑗 ) ∼ ( lastS ‘ 𝑐 ) )
21 fveq2 ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ♯ ‘ 𝑐 ) = ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
22 21 oveq2d ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( 0 ..^ ( ♯ ‘ 𝑐 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
23 fveq1 ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( 𝑐 ‘ 𝑗 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) )
24 fveq2 ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( lastS ‘ 𝑐 ) = ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
25 23 24 breq12d ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ( 𝑐 ‘ 𝑗 ) ∼ ( lastS ‘ 𝑐 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
26 22 25 raleqbidv ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑐 ) ) ( 𝑐 ‘ 𝑗 ) ∼ ( lastS ‘ 𝑐 ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
27 20 26 bitrid ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑐 ) ) ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
28 fveq2 ⊢ ( 𝑐 = 𝐶 → ( ♯ ‘ 𝑐 ) = ( ♯ ‘ 𝐶 ) )
29 28 oveq2d ⊢ ( 𝑐 = 𝐶 → ( 0 ..^ ( ♯ ‘ 𝑐 ) ) = ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
30 fveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑖 ) )
31 fveq2 ⊢ ( 𝑐 = 𝐶 → ( lastS ‘ 𝑐 ) = ( lastS ‘ 𝐶 ) )
32 30 31 breq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ( 𝐶 ‘ 𝑖 ) ∼ ( lastS ‘ 𝐶 ) ) )
33 29 32 raleqbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑐 ) ) ( 𝑐 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑐 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑖 ) ∼ ( lastS ‘ 𝐶 ) ) )
34 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
35 0nnn ⊢ ¬ 0 ∈ ℕ
36 34 35 eqneltri ⊢ ¬ ( ♯ ‘ ∅ ) ∈ ℕ
37 fzo0n0 ⊢ ( ( 0 ..^ ( ♯ ‘ ∅ ) ) ≠ ∅ ↔ ( ♯ ‘ ∅ ) ∈ ℕ )
38 36 37 mtbir ⊢ ¬ ( 0 ..^ ( ♯ ‘ ∅ ) ) ≠ ∅
39 nne ⊢ ( ¬ ( 0 ..^ ( ♯ ‘ ∅ ) ) ≠ ∅ ↔ ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅ )
40 38 39 mpbi ⊢ ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅
41 rzal ⊢ ( ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅ → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∼ ( lastS ‘ ∅ ) )
42 40 41 mp1i ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∼ ( lastS ‘ ∅ ) )
43 1 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ∼ Er 𝐴 )
44 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑥 ∈ 𝐴 )
45 43 44 erref ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑥 ∼ 𝑥 )
46 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
47 46 chnwrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑑 ∈ Word 𝐴 )
48 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
49 ccatws1len ⊢ ( 𝑑 ∈ Word 𝐴 → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
50 47 49 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
51 fveq2 ⊢ ( 𝑑 = ∅ → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ ∅ ) )
52 51 34 eqtr2di ⊢ ( 𝑑 = ∅ → 0 = ( ♯ ‘ 𝑑 ) )
53 52 eqcomd ⊢ ( 𝑑 = ∅ → ( ♯ ‘ 𝑑 ) = 0 )
54 53 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ 𝑑 ) = 0 )
55 54 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ( ♯ ‘ 𝑑 ) + 1 ) = ( 0 + 1 ) )
56 0p1e1 ⊢ ( 0 + 1 ) = 1
57 55 56 eqtrdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ( ♯ ‘ 𝑑 ) + 1 ) = 1 )
58 50 57 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 1 )
59 58 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) = ( 0 ..^ 1 ) )
60 48 59 eleqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 ∈ ( 0 ..^ 1 ) )
61 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
62 60 61 eleqtrdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 ∈ { 0 } )
63 62 elsnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 = 0 )
64 52 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 0 = ( ♯ ‘ 𝑑 ) )
65 63 64 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 = ( ♯ ‘ 𝑑 ) )
66 ccats1val2 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = 𝑥 )
67 47 44 65 66 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = 𝑥 )
68 lswccats1 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
69 47 44 68 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
70 45 67 69 3brtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
71 1 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ∼ Er 𝐴 )
72 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
73 72 chnwrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑑 ∈ Word 𝐴 )
74 73 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → 𝑑 ∈ Word 𝐴 )
75 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → 𝑥 ∈ 𝐴 )
76 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → 𝑗 = ( ♯ ‘ 𝑑 ) )
77 74 75 76 66 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = 𝑥 )
78 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) )
79 neneq ⊢ ( 𝑑 ≠ ∅ → ¬ 𝑑 = ∅ )
80 79 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ¬ 𝑑 = ∅ )
81 78 80 orcnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( lastS ‘ 𝑑 ) ∼ 𝑥 )
82 71 81 ersym ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑥 ∼ ( lastS ‘ 𝑑 ) )
83 82 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → 𝑥 ∼ ( lastS ‘ 𝑑 ) )
84 77 83 eqbrtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ 𝑑 ) )
85 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) )
86 85 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ 𝑑 ) ) )
87 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) )
88 simplr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
89 88 chnwrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → 𝑑 ∈ Word 𝐴 )
90 simpr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
91 ccats1val1 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
92 89 90 91 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
93 92 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( 𝑑 ‘ 𝑖 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) )
94 93 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) )
95 94 ralbidva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) )
96 95 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) )
97 87 96 mpbid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) )
98 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
99 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
100 99 chnwrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → 𝑑 ∈ Word 𝐴 )
101 100 49 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
102 101 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
103 98 102 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
104 103 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
105 simp-7r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
106 105 chnwrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑑 ∈ Word 𝐴 )
107 lencl ⊢ ( 𝑑 ∈ Word 𝐴 → ( ♯ ‘ 𝑑 ) ∈ ℕ0 )
108 elnn0uz ⊢ ( ( ♯ ‘ 𝑑 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ 0 ) )
109 108 biimpi ⊢ ( ( ♯ ‘ 𝑑 ) ∈ ℕ0 → ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ 0 ) )
110 106 107 109 3syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ 0 ) )
111 fzosplitsni ⊢ ( ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ 0 ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ∨ 𝑗 = ( ♯ ‘ 𝑑 ) ) ) )
112 110 111 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ∨ 𝑗 = ( ♯ ‘ 𝑑 ) ) ) )
113 104 112 mpbid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ∨ 𝑗 = ( ♯ ‘ 𝑑 ) ) )
114 df-ne ⊢ ( 𝑗 ≠ ( ♯ ‘ 𝑑 ) ↔ ¬ 𝑗 = ( ♯ ‘ 𝑑 ) )
115 114 bilani ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ¬ 𝑗 = ( ♯ ‘ 𝑑 ) )
116 113 115 olcnd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
117 86 97 116 rspcdva ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ 𝑑 ) )
118 84 117 pm2.61dane ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ 𝑑 ) )
119 71 118 81 ertrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ 𝑥 )
120 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑥 ∈ 𝐴 )
121 73 120 68 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
122 119 121 breqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
123 70 122 pm2.61dane ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
124 123 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
125 11 17 27 33 2 42 124 chnind ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑖 ) ∼ ( lastS ‘ 𝐶 ) )
126 5 125 3 rspcdva ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∼ ( lastS ‘ 𝐶 ) )