Metamath Proof Explorer

Theorem chnub

Description: In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnub.1 ⊢ ( 𝜑 → < Po 𝐴 )
chnub.2 ⊢ ( 𝜑 → 𝐶 ∈ ( < Chain 𝐴 ) )
chnub.3 ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐶 ) − 1 ) ) )
Assertion chnub ( 𝜑 → ( 𝐶 ‘ 𝐼 ) < ( lastS ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 chnub.1 ⊢ ( 𝜑 → < Po 𝐴 )
2 chnub.2 ⊢ ( 𝜑 → 𝐶 ∈ ( < Chain 𝐴 ) )
3 chnub.3 ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐶 ) − 1 ) ) )
4 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝐼 ) )
5 4 breq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝐶 ‘ 𝑖 ) < ( lastS ‘ 𝐶 ) ↔ ( 𝐶 ‘ 𝐼 ) < ( lastS ‘ 𝐶 ) ) )
6 fveq2 ⊢ ( 𝑐 = ∅ → ( ♯ ‘ 𝑐 ) = ( ♯ ‘ ∅ ) )
7 6 oveq1d ⊢ ( 𝑐 = ∅ → ( ( ♯ ‘ 𝑐 ) − 1 ) = ( ( ♯ ‘ ∅ ) − 1 ) )
8 7 oveq2d ⊢ ( 𝑐 = ∅ → ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ ∅ ) − 1 ) ) )
9 fveq1 ⊢ ( 𝑐 = ∅ → ( 𝑐 ‘ 𝑖 ) = ( ∅ ‘ 𝑖 ) )
10 fveq2 ⊢ ( 𝑐 = ∅ → ( lastS ‘ 𝑐 ) = ( lastS ‘ ∅ ) )
11 9 10 breq12d ⊢ ( 𝑐 = ∅ → ( ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ( ∅ ‘ 𝑖 ) < ( lastS ‘ ∅ ) ) )
12 8 11 raleqbidv ⊢ ( 𝑐 = ∅ → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ∅ ) − 1 ) ) ( ∅ ‘ 𝑖 ) < ( lastS ‘ ∅ ) ) )
13 fveq2 ⊢ ( 𝑐 = 𝑑 → ( ♯ ‘ 𝑐 ) = ( ♯ ‘ 𝑑 ) )
14 13 oveq1d ⊢ ( 𝑐 = 𝑑 → ( ( ♯ ‘ 𝑐 ) − 1 ) = ( ( ♯ ‘ 𝑑 ) − 1 ) )
15 14 oveq2d ⊢ ( 𝑐 = 𝑑 → ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
16 fveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
17 fveq2 ⊢ ( 𝑐 = 𝑑 → ( lastS ‘ 𝑐 ) = ( lastS ‘ 𝑑 ) )
18 16 17 breq12d ⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) )
19 15 18 raleqbidv ⊢ ( 𝑐 = 𝑑 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) )
20 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑗 ) )
21 20 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ( 𝑐 ‘ 𝑗 ) < ( lastS ‘ 𝑐 ) ) )
22 21 cbvralvw ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) ( 𝑐 ‘ 𝑗 ) < ( lastS ‘ 𝑐 ) )
23 fveq2 ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ♯ ‘ 𝑐 ) = ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
24 23 oveq1d ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ( ♯ ‘ 𝑐 ) − 1 ) = ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) )
25 24 oveq2d ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) )
26 fveq1 ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( 𝑐 ‘ 𝑗 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) )
27 fveq2 ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( lastS ‘ 𝑐 ) = ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
28 26 27 breq12d ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ( 𝑐 ‘ 𝑗 ) < ( lastS ‘ 𝑐 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
29 25 28 raleqbidv ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) ( 𝑐 ‘ 𝑗 ) < ( lastS ‘ 𝑐 ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
30 22 29 bitrid ⊢ ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
31 fveq2 ⊢ ( 𝑐 = 𝐶 → ( ♯ ‘ 𝑐 ) = ( ♯ ‘ 𝐶 ) )
32 31 oveq1d ⊢ ( 𝑐 = 𝐶 → ( ( ♯ ‘ 𝑐 ) − 1 ) = ( ( ♯ ‘ 𝐶 ) − 1 ) )
33 32 oveq2d ⊢ ( 𝑐 = 𝐶 → ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐶 ) − 1 ) ) )
34 fveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑖 ) )
35 fveq2 ⊢ ( 𝑐 = 𝐶 → ( lastS ‘ 𝑐 ) = ( lastS ‘ 𝐶 ) )
36 34 35 breq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ( 𝐶 ‘ 𝑖 ) < ( lastS ‘ 𝐶 ) ) )
37 33 36 raleqbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑐 ) − 1 ) ) ( 𝑐 ‘ 𝑖 ) < ( lastS ‘ 𝑐 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐶 ) − 1 ) ) ( 𝐶 ‘ 𝑖 ) < ( lastS ‘ 𝐶 ) ) )
38 ral0 ⊢ ∀ 𝑖 ∈ ∅ ( ∅ ‘ 𝑖 ) < ( lastS ‘ ∅ )
39 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
40 39 oveq1i ⊢ ( ( ♯ ‘ ∅ ) − 1 ) = ( 0 − 1 )
41 df-neg ⊢ - 1 = ( 0 − 1 )
42 neg1rr ⊢ - 1 ∈ ℝ
43 0re ⊢ 0 ∈ ℝ
44 neg1lt0 ⊢ - 1 < 0
45 42 43 44 ltleii ⊢ - 1 ≤ 0
46 41 45 eqbrtrri ⊢ ( 0 − 1 ) ≤ 0
47 40 46 eqbrtri ⊢ ( ( ♯ ‘ ∅ ) − 1 ) ≤ 0
48 0z ⊢ 0 ∈ ℤ
49 39 48 eqeltri ⊢ ( ♯ ‘ ∅ ) ∈ ℤ
50 1z ⊢ 1 ∈ ℤ
51 zsubcl ⊢ ( ( ( ♯ ‘ ∅ ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ♯ ‘ ∅ ) − 1 ) ∈ ℤ )
52 49 50 51 mp2an ⊢ ( ( ♯ ‘ ∅ ) − 1 ) ∈ ℤ
53 fzon ⊢ ( ( 0 ∈ ℤ ∧ ( ( ♯ ‘ ∅ ) − 1 ) ∈ ℤ ) → ( ( ( ♯ ‘ ∅ ) − 1 ) ≤ 0 ↔ ( 0 ..^ ( ( ♯ ‘ ∅ ) − 1 ) ) = ∅ ) )
54 48 52 53 mp2an ⊢ ( ( ( ♯ ‘ ∅ ) − 1 ) ≤ 0 ↔ ( 0 ..^ ( ( ♯ ‘ ∅ ) − 1 ) ) = ∅ )
55 47 54 mpbi ⊢ ( 0 ..^ ( ( ♯ ‘ ∅ ) − 1 ) ) = ∅
56 55 raleqi ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ∅ ) − 1 ) ) ( ∅ ‘ 𝑖 ) < ( lastS ‘ ∅ ) ↔ ∀ 𝑖 ∈ ∅ ( ∅ ‘ 𝑖 ) < ( lastS ‘ ∅ ) )
57 38 56 mpbir ⊢ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ∅ ) − 1 ) ) ( ∅ ‘ 𝑖 ) < ( lastS ‘ ∅ )
58 57 a1i ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ∅ ) − 1 ) ) ( ∅ ‘ 𝑖 ) < ( lastS ‘ ∅ ) )
59 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → 𝑑 ∈ ( < Chain 𝐴 ) )
60 59 chnwrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → 𝑑 ∈ Word 𝐴 )
61 ccatws1len ⊢ ( 𝑑 ∈ Word 𝐴 → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
62 60 61 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
63 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → 𝑑 = ∅ )
64 63 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ ∅ ) )
65 64 39 eqtrdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ 𝑑 ) = 0 )
66 65 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( ( ♯ ‘ 𝑑 ) + 1 ) = ( 0 + 1 ) )
67 0p1e1 ⊢ ( 0 + 1 ) = 1
68 67 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( 0 + 1 ) = 1 )
69 62 66 68 3eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 1 )
70 69 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) = ( 1 − 1 ) )
71 1m1e0 ⊢ ( 1 − 1 ) = 0
72 70 71 eqtrdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) = 0 )
73 72 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) = ( 0 ..^ 0 ) )
74 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
75 73 74 eqtrdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) = ∅ )
76 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) )
77 76 ne0d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ≠ ∅ )
78 75 77 pm2.21ddne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 = ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
79 1 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → < Po 𝐴 )
80 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑑 ∈ ( < Chain 𝐴 ) )
81 80 chnwrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑑 ∈ Word 𝐴 )
82 81 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → 𝑑 ∈ Word 𝐴 )
83 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑥 ∈ 𝐴 )
84 83 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → 𝑥 ∈ 𝐴 )
85 ccatws1cl ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∈ Word 𝐴 )
86 82 84 85 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∈ Word 𝐴 )
87 lencl ⊢ ( 𝑑 ∈ Word 𝐴 → ( ♯ ‘ 𝑑 ) ∈ ℕ0 )
88 81 87 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ∈ ℕ0 )
89 88 nn0zd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ∈ ℤ )
90 1zzd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 1 ∈ ℤ )
91 89 90 zsubcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ℤ )
92 89 peano2zd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ 𝑑 ) + 1 ) ∈ ℤ )
93 91 zred ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ℝ )
94 92 zred ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ 𝑑 ) + 1 ) ∈ ℝ )
95 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑑 ≠ ∅ )
96 hasheq0 ⊢ ( 𝑑 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑑 ) = 0 ↔ 𝑑 = ∅ ) )
97 96 necon3bid ⊢ ( 𝑑 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑑 ) ≠ 0 ↔ 𝑑 ≠ ∅ ) )
98 97 biimpar ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ≠ 0 )
99 81 95 98 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ≠ 0 )
100 elnnne0 ⊢ ( ( ♯ ‘ 𝑑 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑑 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑑 ) ≠ 0 ) )
101 88 99 100 sylanbrc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ∈ ℕ )
102 101 nnred ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ∈ ℝ )
103 102 ltm1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ 𝑑 ) − 1 ) < ( ♯ ‘ 𝑑 ) )
104 102 ltp1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) < ( ( ♯ ‘ 𝑑 ) + 1 ) )
105 93 102 94 103 104 lttrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ 𝑑 ) − 1 ) < ( ( ♯ ‘ 𝑑 ) + 1 ) )
106 93 94 105 ltled ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ 𝑑 ) − 1 ) ≤ ( ( ♯ ‘ 𝑑 ) + 1 ) )
107 eluz2 ⊢ ( ( ( ♯ ‘ 𝑑 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ↔ ( ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑑 ) + 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑑 ) − 1 ) ≤ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
108 91 92 106 107 syl3anbrc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ 𝑑 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
109 fzoss2 ⊢ ( ( ( ♯ ‘ 𝑑 ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
110 108 109 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
111 110 sselda ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
112 82 61 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
113 112 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
114 111 113 eleqtrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
115 wrdsymbcl ⊢ ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∈ Word 𝐴 ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∈ 𝐴 )
116 86 114 115 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∈ 𝐴 )
117 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → 𝑑 ≠ ∅ )
118 lswcl ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅ ) → ( lastS ‘ 𝑑 ) ∈ 𝐴 )
119 82 117 118 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( lastS ‘ 𝑑 ) ∈ 𝐴 )
120 lswccats1 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
121 81 83 120 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
122 121 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
123 122 84 eqeltrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ∈ 𝐴 )
124 116 119 123 3jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∈ 𝐴 ∧ ( lastS ‘ 𝑑 ) ∈ 𝐴 ∧ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ∈ 𝐴 ) )
125 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) )
126 61 oveq1d ⊢ ( 𝑑 ∈ Word 𝐴 → ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑑 ) + 1 ) − 1 ) )
127 81 126 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) = ( ( ( ♯ ‘ 𝑑 ) + 1 ) − 1 ) )
128 101 nncnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ∈ ℂ )
129 1cnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 1 ∈ ℂ )
130 128 129 pncand ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ( ♯ ‘ 𝑑 ) + 1 ) − 1 ) = ( ♯ ‘ 𝑑 ) )
131 127 130 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) = ( ♯ ‘ 𝑑 ) )
132 131 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
133 125 132 eleqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
134 133 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
135 ccats1val1 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = ( 𝑑 ‘ 𝑗 ) )
136 82 134 135 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = ( 𝑑 ‘ 𝑗 ) )
137 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑑 ‘ 𝑖 ) = ( 𝑑 ‘ 𝑗 ) )
138 137 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ↔ ( 𝑑 ‘ 𝑗 ) < ( lastS ‘ 𝑑 ) ) )
139 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) )
140 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
141 138 139 140 rspcdva ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( 𝑑 ‘ 𝑗 ) < ( lastS ‘ 𝑑 ) )
142 136 141 eqbrtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ 𝑑 ) )
143 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) )
144 95 neneqd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ¬ 𝑑 = ∅ )
145 143 144 orcnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( lastS ‘ 𝑑 ) < 𝑥 )
146 145 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( lastS ‘ 𝑑 ) < 𝑥 )
147 146 122 breqtrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( lastS ‘ 𝑑 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
148 potr ⊢ ( ( < Po 𝐴 ∧ ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∈ 𝐴 ∧ ( lastS ‘ 𝑑 ) ∈ 𝐴 ∧ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ∈ 𝐴 ) ) → ( ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ 𝑑 ) ∧ ( lastS ‘ 𝑑 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) )
149 148 imp ⊢ ( ( ( < Po 𝐴 ∧ ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ∈ 𝐴 ∧ ( lastS ‘ 𝑑 ) ∈ 𝐴 ∧ ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ∈ 𝐴 ) ) ∧ ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ 𝑑 ) ∧ ( lastS ‘ 𝑑 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
150 79 124 142 147 149 syl22anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
151 145 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( lastS ‘ 𝑑 ) < 𝑥 )
152 81 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → 𝑑 ∈ Word 𝐴 )
153 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → 𝑥 ∈ 𝐴 )
154 153 s1cld ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ⟨“ 𝑥 ”⟩ ∈ Word 𝐴 )
155 101 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( ♯ ‘ 𝑑 ) ∈ ℕ )
156 fzo0end ⊢ ( ( ♯ ‘ 𝑑 ) ∈ ℕ → ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
157 155 156 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
158 ccatval1 ⊢ ( ( 𝑑 ∈ Word 𝐴 ∧ ⟨“ 𝑥 ”⟩ ∈ Word 𝐴 ∧ ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
159 152 154 157 158 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
160 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) )
161 160 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
162 lsw ⊢ ( 𝑑 ∈ Word 𝐴 → ( lastS ‘ 𝑑 ) = ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
163 152 162 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( lastS ‘ 𝑑 ) = ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
164 159 161 163 3eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = ( lastS ‘ 𝑑 ) )
165 121 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = 𝑥 )
166 151 164 165 3brtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) ∧ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
167 67 fveq2i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
168 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
169 167 168 eqtr4i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ℕ
170 101 169 eleqtrrdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
171 fzosplitsnm1 ⊢ ( ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝑑 ) ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑑 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑑 ) − 1 ) } ) )
172 48 170 171 sylancr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( 0 ..^ ( ♯ ‘ 𝑑 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑑 ) − 1 ) } ) )
173 133 172 eleqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → 𝑗 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑑 ) − 1 ) } ) )
174 elunsn ⊢ ( 𝑗 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑑 ) − 1 ) } ) → ( 𝑗 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑑 ) − 1 ) } ) ↔ ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∨ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) )
175 174 ibi ⊢ ( 𝑗 ∈ ( ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑑 ) − 1 ) } ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∨ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
176 173 175 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ∨ 𝑗 = ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
177 150 166 176 mpjaodan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) ∧ 𝑑 ≠ ∅ ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
178 78 177 pm2.61dane ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
179 178 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ( 𝑑 ‘ 𝑖 ) < ( lastS ‘ 𝑑 ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) − 1 ) ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) < ( lastS ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
180 12 19 30 37 2 58 179 chnind ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐶 ) − 1 ) ) ( 𝐶 ‘ 𝑖 ) < ( lastS ‘ 𝐶 ) )
181 5 180 3 rspcdva ⊢ ( 𝜑 → ( 𝐶 ‘ 𝐼 ) < ( lastS ‘ 𝐶 ) )