Metamath Proof Explorer


Theorem chnind

Description: Induction over a chain. See nnind for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnind.1 ( 𝑐 = ∅ → ( 𝜓𝜒 ) )
chnind.2 ( 𝑐 = 𝑑 → ( 𝜓𝜃 ) )
chnind.3 ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( 𝜓𝜏 ) )
chnind.4 ( 𝑐 = 𝐶 → ( 𝜓𝜂 ) )
chnind.6 ( 𝜑𝐶 ∈ ( < Chain 𝐴 ) )
chnind.7 ( 𝜑𝜒 )
chnind.8 ( ( ( ( ( 𝜑𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ 𝜃 ) → 𝜏 )
Assertion chnind ( 𝜑𝜂 )

Proof

Step Hyp Ref Expression
1 chnind.1 ( 𝑐 = ∅ → ( 𝜓𝜒 ) )
2 chnind.2 ( 𝑐 = 𝑑 → ( 𝜓𝜃 ) )
3 chnind.3 ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( 𝜓𝜏 ) )
4 chnind.4 ( 𝑐 = 𝐶 → ( 𝜓𝜂 ) )
5 chnind.6 ( 𝜑𝐶 ∈ ( < Chain 𝐴 ) )
6 chnind.7 ( 𝜑𝜒 )
7 chnind.8 ( ( ( ( ( 𝜑𝑑 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥𝐴 ) ∧ ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) ) ∧ 𝜃 ) → 𝜏 )
8 5 chnwrd ( 𝜑𝐶 ∈ Word 𝐴 )
9 id ( 𝜑𝜑 )
10 ischn ( 𝐶 ∈ ( < Chain 𝐴 ) ↔ ( 𝐶 ∈ Word 𝐴 ∧ ∀ 𝑖 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) ) )
11 5 10 sylib ( 𝜑 → ( 𝐶 ∈ Word 𝐴 ∧ ∀ 𝑖 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) ) )
12 11 simprd ( 𝜑 → ∀ 𝑖 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) )
13 dmeq ( 𝑐 = ∅ → dom 𝑐 = dom ∅ )
14 13 difeq1d ( 𝑐 = ∅ → ( dom 𝑐 ∖ { 0 } ) = ( dom ∅ ∖ { 0 } ) )
15 fveq1 ( 𝑐 = ∅ → ( 𝑐 ‘ ( 𝑖 − 1 ) ) = ( ∅ ‘ ( 𝑖 − 1 ) ) )
16 fveq1 ( 𝑐 = ∅ → ( 𝑐𝑖 ) = ( ∅ ‘ 𝑖 ) )
17 15 16 breq12d ( 𝑐 = ∅ → ( ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ↔ ( ∅ ‘ ( 𝑖 − 1 ) ) < ( ∅ ‘ 𝑖 ) ) )
18 14 17 raleqbidv ( 𝑐 = ∅ → ( ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ↔ ∀ 𝑖 ∈ ( dom ∅ ∖ { 0 } ) ( ∅ ‘ ( 𝑖 − 1 ) ) < ( ∅ ‘ 𝑖 ) ) )
19 18 anbi2d ( 𝑐 = ∅ → ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ) ↔ ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom ∅ ∖ { 0 } ) ( ∅ ‘ ( 𝑖 − 1 ) ) < ( ∅ ‘ 𝑖 ) ) ) )
20 19 1 imbi12d ( 𝑐 = ∅ → ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ) → 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom ∅ ∖ { 0 } ) ( ∅ ‘ ( 𝑖 − 1 ) ) < ( ∅ ‘ 𝑖 ) ) → 𝜒 ) ) )
21 dmeq ( 𝑐 = 𝑑 → dom 𝑐 = dom 𝑑 )
22 21 difeq1d ( 𝑐 = 𝑑 → ( dom 𝑐 ∖ { 0 } ) = ( dom 𝑑 ∖ { 0 } ) )
23 fveq1 ( 𝑐 = 𝑑 → ( 𝑐 ‘ ( 𝑖 − 1 ) ) = ( 𝑑 ‘ ( 𝑖 − 1 ) ) )
24 fveq1 ( 𝑐 = 𝑑 → ( 𝑐𝑖 ) = ( 𝑑𝑖 ) )
25 23 24 breq12d ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ↔ ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) ) )
26 22 25 raleqbidv ( 𝑐 = 𝑑 → ( ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ↔ ∀ 𝑖 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) ) )
27 26 anbi2d ( 𝑐 = 𝑑 → ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ) ↔ ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) ) ) )
28 27 2 imbi12d ( 𝑐 = 𝑑 → ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ) → 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) ) → 𝜃 ) ) )
29 dmeq ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → dom 𝑐 = dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) )
30 29 difeq1d ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( dom 𝑐 ∖ { 0 } ) = ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) )
31 fveq1 ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( 𝑐 ‘ ( 𝑖 − 1 ) ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) )
32 fveq1 ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( 𝑐𝑖 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) )
33 31 32 breq12d ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) )
34 30 33 raleqbidv ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ↔ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) )
35 34 anbi2d ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ) ↔ ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ) )
36 35 3 imbi12d ( 𝑐 = ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) → ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ) → 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝜏 ) ) )
37 dmeq ( 𝑐 = 𝐶 → dom 𝑐 = dom 𝐶 )
38 37 difeq1d ( 𝑐 = 𝐶 → ( dom 𝑐 ∖ { 0 } ) = ( dom 𝐶 ∖ { 0 } ) )
39 fveq1 ( 𝑐 = 𝐶 → ( 𝑐 ‘ ( 𝑖 − 1 ) ) = ( 𝐶 ‘ ( 𝑖 − 1 ) ) )
40 fveq1 ( 𝑐 = 𝐶 → ( 𝑐𝑖 ) = ( 𝐶𝑖 ) )
41 39 40 breq12d ( 𝑐 = 𝐶 → ( ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ↔ ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) ) )
42 38 41 raleqbidv ( 𝑐 = 𝐶 → ( ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ↔ ∀ 𝑖 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) ) )
43 42 anbi2d ( 𝑐 = 𝐶 → ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ) ↔ ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) ) ) )
44 43 4 imbi12d ( 𝑐 = 𝐶 → ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑖 − 1 ) ) < ( 𝑐𝑖 ) ) → 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) ) → 𝜂 ) ) )
45 6 adantr ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom ∅ ∖ { 0 } ) ( ∅ ‘ ( 𝑖 − 1 ) ) < ( ∅ ‘ 𝑖 ) ) → 𝜒 )
46 simpllr ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → 𝜑 )
47 simp-4l ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → 𝑑 ∈ Word 𝐴 )
48 simpll ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) → 𝑑 ∈ Word 𝐴 )
49 simplr ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) → 𝑥𝐴 )
50 49 s1cld ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) → ⟨“ 𝑥 ”⟩ ∈ Word 𝐴 )
51 48 50 ccatdmss ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) → dom 𝑑 ⊆ dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) )
52 51 ssdifd ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) → ( dom 𝑑 ∖ { 0 } ) ⊆ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) )
53 52 sselda ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) → 𝑗 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) )
54 fvoveq1 ( 𝑖 = 𝑗 → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑗 − 1 ) ) )
55 fveq2 ( 𝑖 = 𝑗 → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) )
56 54 55 breq12d ( 𝑖 = 𝑗 → ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑗 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ) )
57 56 adantl ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ 𝑖 = 𝑗 ) → ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑗 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ) )
58 53 57 rspcdv ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) → ( ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑗 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) ) )
59 58 imp ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑗 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) )
60 simp-4l ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑑 ∈ Word 𝐴 )
61 50 ad2antrr ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ⟨“ 𝑥 ”⟩ ∈ Word 𝐴 )
62 lencl ( 𝑑 ∈ Word 𝐴 → ( ♯ ‘ 𝑑 ) ∈ ℕ0 )
63 60 62 syl ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ♯ ‘ 𝑑 ) ∈ ℕ0 )
64 63 nn0zd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ♯ ‘ 𝑑 ) ∈ ℤ )
65 fzossrbm1 ( ( ♯ ‘ 𝑑 ) ∈ ℤ → ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
66 64 65 syl ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
67 fzossz ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ⊆ ℤ
68 simplr ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) )
69 68 eldifad ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑗 ∈ dom 𝑑 )
70 eqidd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑑 ) )
71 70 60 wrdfd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑑 : ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ⟶ 𝐴 )
72 71 fdmd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → dom 𝑑 = ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
73 69 72 eleqtrd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
74 67 73 sselid ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑗 ∈ ℤ )
75 eldifsni ( 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) → 𝑗 ≠ 0 )
76 68 75 syl ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑗 ≠ 0 )
77 fzo1fzo0n0 ( 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑑 ) ) ↔ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ∧ 𝑗 ≠ 0 ) )
78 73 76 77 sylanbrc ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑑 ) ) )
79 elfzom1b ( ( 𝑗 ∈ ℤ ∧ ( ♯ ‘ 𝑑 ) ∈ ℤ ) → ( 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑑 ) ) ↔ ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) ) )
80 79 biimpa ( ( ( 𝑗 ∈ ℤ ∧ ( ♯ ‘ 𝑑 ) ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
81 74 64 78 80 syl21anc ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
82 66 81 sseldd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
83 ccatval1 ( ( 𝑑 ∈ Word 𝐴 ∧ ⟨“ 𝑥 ”⟩ ∈ Word 𝐴 ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑗 − 1 ) ) = ( 𝑑 ‘ ( 𝑗 − 1 ) ) )
84 60 61 82 83 syl3anc ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑗 − 1 ) ) = ( 𝑑 ‘ ( 𝑗 − 1 ) ) )
85 ccatval1 ( ( 𝑑 ∈ Word 𝐴 ∧ ⟨“ 𝑥 ”⟩ ∈ Word 𝐴𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = ( 𝑑𝑗 ) )
86 60 61 73 85 syl3anc ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑗 ) = ( 𝑑𝑗 ) )
87 59 84 86 3brtr3d ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) )
88 87 an32s ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) → ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) )
89 88 adantllr ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ) → ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) )
90 89 ralrimiva ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ∀ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) )
91 90 an32s ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → ∀ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) )
92 ischn ( 𝑑 ∈ ( < Chain 𝐴 ) ↔ ( 𝑑 ∈ Word 𝐴 ∧ ∀ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) ) )
93 47 91 92 sylanbrc ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → 𝑑 ∈ ( < Chain 𝐴 ) )
94 46 93 jca ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → ( 𝜑𝑑 ∈ ( < Chain 𝐴 ) ) )
95 simp-4r ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → 𝑥𝐴 )
96 lsw ( 𝑑 ∈ Word 𝐴 → ( lastS ‘ 𝑑 ) = ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
97 96 ad5antr ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( lastS ‘ 𝑑 ) = ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
98 simp-4l ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → 𝑑 ∈ Word 𝐴 )
99 fzonn0p1 ( ( ♯ ‘ 𝑑 ) ∈ ℕ0 → ( ♯ ‘ 𝑑 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
100 98 62 99 3syl ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( ♯ ‘ 𝑑 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
101 ccatws1len ( 𝑑 ∈ Word 𝐴 → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
102 101 ad4antr ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) = ( ( ♯ ‘ 𝑑 ) + 1 ) )
103 102 eqcomd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( ( ♯ ‘ 𝑑 ) + 1 ) = ( ♯ ‘ ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ) )
104 ccatws1cl ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) → ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∈ Word 𝐴 )
105 104 ad3antrrr ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∈ Word 𝐴 )
106 103 105 wrdfd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) : ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) ⟶ 𝐴 )
107 106 fdmd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) = ( 0 ..^ ( ( ♯ ‘ 𝑑 ) + 1 ) ) )
108 100 107 eleqtrrd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( ♯ ‘ 𝑑 ) ∈ dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) )
109 simplr ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ¬ 𝑑 = ∅ )
110 109 neqned ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → 𝑑 ≠ ∅ )
111 hasheq0 ( 𝑑 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑑 ) = 0 ↔ 𝑑 = ∅ ) )
112 111 necon3bid ( 𝑑 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑑 ) ≠ 0 ↔ 𝑑 ≠ ∅ ) )
113 112 biimpar ( ( 𝑑 ∈ Word 𝐴𝑑 ≠ ∅ ) → ( ♯ ‘ 𝑑 ) ≠ 0 )
114 98 110 113 syl2anc ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( ♯ ‘ 𝑑 ) ≠ 0 )
115 108 114 eldifsnd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( ♯ ‘ 𝑑 ) ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) )
116 fvoveq1 ( 𝑖 = ( ♯ ‘ 𝑑 ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
117 fveq2 ( 𝑖 = ( ♯ ‘ 𝑑 ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ♯ ‘ 𝑑 ) ) )
118 116 117 breq12d ( 𝑖 = ( ♯ ‘ 𝑑 ) → ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ♯ ‘ 𝑑 ) ) ) )
119 118 adantl ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ 𝑖 = ( ♯ ‘ 𝑑 ) ) → ( ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ↔ ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ♯ ‘ 𝑑 ) ) ) )
120 115 119 rspcdv ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) → ( ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ♯ ‘ 𝑑 ) ) ) )
121 120 imp ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ♯ ‘ 𝑑 ) ) )
122 48 ad3antrrr ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑑 ∈ Word 𝐴 )
123 50 ad3antrrr ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ⟨“ 𝑥 ”⟩ ∈ Word 𝐴 )
124 122 62 syl ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ♯ ‘ 𝑑 ) ∈ ℕ0 )
125 114 adantr ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ♯ ‘ 𝑑 ) ≠ 0 )
126 elnnne0 ( ( ♯ ‘ 𝑑 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑑 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑑 ) ≠ 0 ) )
127 124 125 126 sylanbrc ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ♯ ‘ 𝑑 ) ∈ ℕ )
128 fzo0end ( ( ♯ ‘ 𝑑 ) ∈ ℕ → ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
129 127 128 syl ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) )
130 ccatval1 ( ( 𝑑 ∈ Word 𝐴 ∧ ⟨“ 𝑥 ”⟩ ∈ Word 𝐴 ∧ ( ( ♯ ‘ 𝑑 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑑 ) ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
131 122 123 129 130 syl3anc ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) = ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) )
132 49 ad3antrrr ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝑥𝐴 )
133 eqidd ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑑 ) )
134 ccats1val2 ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ∧ ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑑 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ♯ ‘ 𝑑 ) ) = 𝑥 )
135 122 132 133 134 syl3anc ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( ♯ ‘ 𝑑 ) ) = 𝑥 )
136 121 131 135 3brtr3d ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( 𝑑 ‘ ( ( ♯ ‘ 𝑑 ) − 1 ) ) < 𝑥 )
137 97 136 eqbrtrd ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ¬ 𝑑 = ∅ ) ∧ 𝜃 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( lastS ‘ 𝑑 ) < 𝑥 )
138 137 an42ds ( ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) ∧ ¬ 𝑑 = ∅ ) → ( lastS ‘ 𝑑 ) < 𝑥 )
139 138 ex ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → ( ¬ 𝑑 = ∅ → ( lastS ‘ 𝑑 ) < 𝑥 ) )
140 139 orrd ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → ( 𝑑 = ∅ ∨ ( lastS ‘ 𝑑 ) < 𝑥 ) )
141 simpr ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → 𝜃 )
142 94 95 140 141 7 syl1111anc ( ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) ∧ 𝜃 ) → 𝜏 )
143 142 ex ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( 𝜃𝜏 ) )
144 143 expl ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) → ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ( 𝜃𝜏 ) ) )
145 88 ralrimiva ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ∀ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) )
146 fvoveq1 ( 𝑖 = 𝑗 → ( 𝑑 ‘ ( 𝑖 − 1 ) ) = ( 𝑑 ‘ ( 𝑗 − 1 ) ) )
147 fveq2 ( 𝑖 = 𝑗 → ( 𝑑𝑖 ) = ( 𝑑𝑗 ) )
148 146 147 breq12d ( 𝑖 = 𝑗 → ( ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) ↔ ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) ) )
149 148 cbvralvw ( ∀ 𝑖 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) ↔ ∀ 𝑗 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑗 − 1 ) ) < ( 𝑑𝑗 ) )
150 145 149 sylibr ( ( ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) ∧ 𝜑 ) ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ∀ 𝑖 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) )
151 150 expl ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) → ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → ∀ 𝑖 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) ) )
152 144 151 a2and ( ( 𝑑 ∈ Word 𝐴𝑥𝐴 ) → ( ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝑑 ∖ { 0 } ) ( 𝑑 ‘ ( 𝑖 − 1 ) ) < ( 𝑑𝑖 ) ) → 𝜃 ) → ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ∖ { 0 } ) ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ ( 𝑖 − 1 ) ) < ( ( 𝑑 ++ ⟨“ 𝑥 ”⟩ ) ‘ 𝑖 ) ) → 𝜏 ) ) )
153 20 28 36 44 45 152 wrdind ( 𝐶 ∈ Word 𝐴 → ( ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) ) → 𝜂 ) )
154 153 imp ( ( 𝐶 ∈ Word 𝐴 ∧ ( 𝜑 ∧ ∀ 𝑖 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑖 − 1 ) ) < ( 𝐶𝑖 ) ) ) → 𝜂 )
155 8 9 12 154 syl12anc ( 𝜑𝜂 )