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 0nnn ⊢ ¬ 0 ∈ ℕ
35 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
36 35 eleq1i ⊢ ( ( ♯ ‘ ∅ ) ∈ ℕ ↔ 0 ∈ ℕ )
37 34 36 mtbir ⊢ ¬ ( ♯ ‘ ∅ ) ∈ ℕ
38 fzo0n0 ⊢ ( ( 0 ..^ ( ♯ ‘ ∅ ) ) ≠ ∅ ↔ ( ♯ ‘ ∅ ) ∈ ℕ )
39 37 38 mtbir ⊢ ¬ ( 0 ..^ ( ♯ ‘ ∅ ) ) ≠ ∅
40 nne ⊢ ( ¬ ( 0 ..^ ( ♯ ‘ ∅ ) ) ≠ ∅ ↔ ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅ )
41 39 40 mpbi ⊢ ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅
42 rzal ⊢ ( ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅ → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∼ ( lastS ‘ ∅ ) )
43 41 42 mp1i ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∼ ( lastS ‘ ∅ ) )
44 1 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ∼ Er 𝐴 )
45 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑥 ∈ 𝐴 )
46 44 45 erref ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑥 ∼ 𝑥 )
47 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
48 47 chnwrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑑 ∈ Word 𝐴 )
49 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
50 ccatws1len ⊢ ( 𝑑 ∈ Word 𝐴 → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
51 48 50 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
52 fveq2 ⊢ ( 𝑑 = ∅ → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ ∅ ) )
53 52 35 eqtr2di ⊢ ( 𝑑 = ∅ → 0 = ( ♯ ‘ 𝑑 ) )
54 53 eqcomd ⊢ ( 𝑑 = ∅ → ( ♯ ‘ 𝑑 ) = 0 )
55 54 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ 𝑑 ) = 0 )
56 55 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ( ♯ ‘ 𝑑 ) + 1 ) = ( 0 + 1 ) )
57 0p1e1 ⊢ ( 0 + 1 ) = 1
58 56 57 eqtrdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ( ♯ ‘ 𝑑 ) + 1 ) = 1 )
59 51 58 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 1 )
60 59 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) = ( 0 ..^ 1 ) )
61 49 60 eleqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 ∈ ( 0 ..^ 1 ) )
62 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
63 62 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( 0 ..^ 1 ) = { 0 } )
64 61 63 eleqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 ∈ { 0 } )
65 elsni ⊢ ( 𝑗 ∈ { 0 } → 𝑗 = 0 )
66 64 65 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 = 0 )
67 53 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 0 = ( ♯ ‘ 𝑑 ) )
68 66 67 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 = ( ♯ ‘ 𝑑 ) )
69 ccats1val2 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = 𝑥 )
70 48 45 68 69 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = 𝑥 )
71 lswccats1 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
72 48 45 71 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
73 46 70 72 3brtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 = ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
74 1 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ∼ Er 𝐴 )
75 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
76 75 chnwrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑑 ∈ Word 𝐴 )
77 76 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → 𝑑 ∈ Word 𝐴 )
78 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → 𝑥 ∈ 𝐴 )
79 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → 𝑗 = ( ♯ ‘ 𝑑 ) )
80 77 78 79 69 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = 𝑥 )
81 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) )
82 neneq ⊢ ( 𝑑 ≠ ∅ → ¬ 𝑑 = ∅ )
83 82 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ¬ 𝑑 = ∅ )
84 81 83 orcnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( lastS ‘ 𝑑 ) ∼ 𝑥 )
85 74 84 ersym ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑥 ∼ ( lastS ‘ 𝑑 ) )
86 85 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → 𝑥 ∼ ( lastS ‘ 𝑑 ) )
87 80 86 eqbrtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ 𝑑 ) )
88 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) )
89 88 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ 𝑑 ) ) )
90 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) )
91 90 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) )
92 simplr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
93 92 chnwrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → 𝑑 ∈ Word 𝐴 )
94 simpr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
95 ccats1val1 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
96 93 94 95 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
97 96 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( 𝑑 ‘ 𝑖 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) )
98 97 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) )
99 98 ralbidva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) )
100 99 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) )
101 91 100 mpbid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) )
102 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
103 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
104 103 chnwrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → 𝑑 ∈ Word 𝐴 )
105 104 50 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
106 105 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
107 102 106 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
108 107 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
109 simp-7r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑑 ∈ ( ∼ Chain 𝐴 ) )
110 109 chnwrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑑 ∈ Word 𝐴 )
111 lencl ⊢ ( 𝑑 ∈ Word 𝐴 → ( ♯ ‘ 𝑑 ) ∈ ℕ0 )
112 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
113 112 eleq2i ⊢ ( ( ♯ ‘ 𝑑 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ 0 ) )
114 113 biimpi ⊢ ( ( ♯ ‘ 𝑑 ) ∈ ℕ0 → ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ 0 ) )
115 110 111 114 3syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ 0 ) )
116 fzosplitsni ⊢ ( ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ 0 ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ∨ 𝑗 = ( ♯ ‘ 𝑑 ) ) ) )
117 115 116 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ∨ 𝑗 = ( ♯ ‘ 𝑑 ) ) ) )
118 108 117 mpbid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ∨ 𝑗 = ( ♯ ‘ 𝑑 ) ) )
119 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑗 ≠ ( ♯ ‘ 𝑑 ) )
120 df-ne ⊢ ( 𝑗 ≠ ( ♯ ‘ 𝑑 ) ↔ ¬ 𝑗 = ( ♯ ‘ 𝑑 ) )
121 119 120 sylib ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ¬ 𝑗 = ( ♯ ‘ 𝑑 ) )
122 118 121 olcnd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
123 89 101 122 rspcdva ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ≠ ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ 𝑑 ) )
124 87 123 pm2.61dane ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ 𝑑 ) )
125 74 124 84 ertrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ 𝑥 )
126 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑥 ∈ 𝐴 )
127 76 126 71 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
128 125 127 breqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
129 73 128 pm2.61dane ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
130 129 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) ∼ 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ( 𝑑 ‘ 𝑖 ) ∼ ( lastS ‘ 𝑑 ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∼ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
131 11 17 27 33 2 43 130 chnind ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑖 ) ∼ ( lastS ‘ 𝐶 ) )
132 5 131 3 rspcdva ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∼ ( lastS ‘ 𝐶 ) )