| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | chnind.6 | . . 3
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) | 
| 2 | 1 | chnwrd 32998 | . 2
⊢ (𝜑 → 𝐶 ∈ Word 𝐴) | 
| 3 |  | id 22 | . 2
⊢ (𝜑 → 𝜑) | 
| 4 |  | ischn 32997 | . . . 4
⊢ (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) | 
| 5 | 1, 4 | sylib 218 | . . 3
⊢ (𝜑 → (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) | 
| 6 | 5 | simprd 495 | . 2
⊢ (𝜑 → ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) | 
| 7 |  | dmeq 5913 | . . . . . . . 8
⊢ (𝑐 = ∅ → dom 𝑐 = dom ∅) | 
| 8 | 7 | difeq1d 4124 | . . . . . . 7
⊢ (𝑐 = ∅ → (dom 𝑐 ∖ {0}) = (dom ∅
∖ {0})) | 
| 9 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = ∅ → (𝑐‘(𝑖 − 1)) = (∅‘(𝑖 − 1))) | 
| 10 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = ∅ → (𝑐‘𝑖) = (∅‘𝑖)) | 
| 11 | 9, 10 | breq12d 5155 | . . . . . . 7
⊢ (𝑐 = ∅ → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (∅‘(𝑖 − 1)) < (∅‘𝑖))) | 
| 12 | 8, 11 | raleqbidv 3345 | . . . . . 6
⊢ (𝑐 = ∅ → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom ∅ ∖
{0})(∅‘(𝑖
− 1)) < (∅‘𝑖))) | 
| 13 | 12 | anbi2d 630 | . . . . 5
⊢ (𝑐 = ∅ → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖
{0})(∅‘(𝑖
− 1)) < (∅‘𝑖)))) | 
| 14 |  | chnind.1 | . . . . 5
⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒)) | 
| 15 | 13, 14 | imbi12d 344 | . . . 4
⊢ (𝑐 = ∅ → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖
{0})(∅‘(𝑖
− 1)) < (∅‘𝑖)) → 𝜒))) | 
| 16 |  | dmeq 5913 | . . . . . . . 8
⊢ (𝑐 = 𝑑 → dom 𝑐 = dom 𝑑) | 
| 17 | 16 | difeq1d 4124 | . . . . . . 7
⊢ (𝑐 = 𝑑 → (dom 𝑐 ∖ {0}) = (dom 𝑑 ∖ {0})) | 
| 18 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = 𝑑 → (𝑐‘(𝑖 − 1)) = (𝑑‘(𝑖 − 1))) | 
| 19 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = 𝑑 → (𝑐‘𝑖) = (𝑑‘𝑖)) | 
| 20 | 18, 19 | breq12d 5155 | . . . . . . 7
⊢ (𝑐 = 𝑑 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))) | 
| 21 | 17, 20 | raleqbidv 3345 | . . . . . 6
⊢ (𝑐 = 𝑑 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))) | 
| 22 | 21 | anbi2d 630 | . . . . 5
⊢ (𝑐 = 𝑑 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))) | 
| 23 |  | chnind.2 | . . . . 5
⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃)) | 
| 24 | 22, 23 | imbi12d 344 | . . . 4
⊢ (𝑐 = 𝑑 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃))) | 
| 25 |  | dmeq 5913 | . . . . . . . 8
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → dom 𝑐 = dom (𝑑 ++ 〈“𝑥”〉)) | 
| 26 | 25 | difeq1d 4124 | . . . . . . 7
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (dom 𝑐 ∖ {0}) = (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})) | 
| 27 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (𝑐‘(𝑖 − 1)) = ((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1))) | 
| 28 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (𝑐‘𝑖) = ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) | 
| 29 | 27, 28 | breq12d 5155 | . . . . . . 7
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖))) | 
| 30 | 26, 29 | raleqbidv 3345 | . . . . . 6
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖))) | 
| 31 | 30 | anbi2d 630 | . . . . 5
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)))) | 
| 32 |  | chnind.3 | . . . . 5
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (𝜓 ↔ 𝜏)) | 
| 33 | 31, 32 | imbi12d 344 | . . . 4
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝜏))) | 
| 34 |  | dmeq 5913 | . . . . . . . 8
⊢ (𝑐 = 𝐶 → dom 𝑐 = dom 𝐶) | 
| 35 | 34 | difeq1d 4124 | . . . . . . 7
⊢ (𝑐 = 𝐶 → (dom 𝑐 ∖ {0}) = (dom 𝐶 ∖ {0})) | 
| 36 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = 𝐶 → (𝑐‘(𝑖 − 1)) = (𝐶‘(𝑖 − 1))) | 
| 37 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑐 = 𝐶 → (𝑐‘𝑖) = (𝐶‘𝑖)) | 
| 38 | 36, 37 | breq12d 5155 | . . . . . . 7
⊢ (𝑐 = 𝐶 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) | 
| 39 | 35, 38 | raleqbidv 3345 | . . . . . 6
⊢ (𝑐 = 𝐶 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) | 
| 40 | 39 | anbi2d 630 | . . . . 5
⊢ (𝑐 = 𝐶 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))) | 
| 41 |  | chnind.4 | . . . . 5
⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂)) | 
| 42 | 40, 41 | imbi12d 344 | . . . 4
⊢ (𝑐 = 𝐶 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂))) | 
| 43 |  | chnind.7 | . . . . 5
⊢ (𝜑 → 𝜒) | 
| 44 | 43 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖
{0})(∅‘(𝑖
− 1)) < (∅‘𝑖)) → 𝜒) | 
| 45 |  | simpllr 775 | . . . . . . . . 9
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → 𝜑) | 
| 46 |  | simp-4l 782 | . . . . . . . . . 10
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ Word 𝐴) | 
| 47 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑑 ∈ Word 𝐴) | 
| 48 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑥 ∈ 𝐴) | 
| 49 | 48 | s1cld 14642 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 〈“𝑥”〉 ∈ Word 𝐴) | 
| 50 | 47, 49 | ccatdmss 32935 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → dom 𝑑 ⊆ dom (𝑑 ++ 〈“𝑥”〉)) | 
| 51 | 50 | ssdifd 4144 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → (dom 𝑑 ∖ {0}) ⊆ (dom (𝑑 ++ 〈“𝑥”〉) ∖
{0})) | 
| 52 | 51 | sselda 3982 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → 𝑗 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})) | 
| 53 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → ((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) = ((𝑑 ++ 〈“𝑥”〉)‘(𝑗 − 1))) | 
| 54 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → ((𝑑 ++ 〈“𝑥”〉)‘𝑖) = ((𝑑 ++ 〈“𝑥”〉)‘𝑗)) | 
| 55 | 53, 54 | breq12d 5155 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑗 → (((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖) ↔ ((𝑑 ++ 〈“𝑥”〉)‘(𝑗 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑗))) | 
| 56 | 55 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ 𝑖 = 𝑗) → (((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖) ↔ ((𝑑 ++ 〈“𝑥”〉)‘(𝑗 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑗))) | 
| 57 | 52, 56 | rspcdv 3613 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖) → ((𝑑 ++ 〈“𝑥”〉)‘(𝑗 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑗))) | 
| 58 | 57 | imp 406 | . . . . . . . . . . . . . . 15
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ((𝑑 ++ 〈“𝑥”〉)‘(𝑗 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑗)) | 
| 59 |  | simp-4l 782 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑑 ∈ Word 𝐴) | 
| 60 | 49 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 〈“𝑥”〉 ∈ Word 𝐴) | 
| 61 |  | lencl 14572 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈
ℕ0) | 
| 62 | 59, 61 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (♯‘𝑑) ∈
ℕ0) | 
| 63 | 62 | nn0zd 12641 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (♯‘𝑑) ∈ ℤ) | 
| 64 |  | fzossrbm1 13729 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑑)
∈ ℤ → (0..^((♯‘𝑑) − 1)) ⊆
(0..^(♯‘𝑑))) | 
| 65 | 63, 64 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (0..^((♯‘𝑑) − 1)) ⊆
(0..^(♯‘𝑑))) | 
| 66 |  | fzossz 13720 | . . . . . . . . . . . . . . . . . . 19
⊢
(0..^(♯‘𝑑)) ⊆ ℤ | 
| 67 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑗 ∈ (dom 𝑑 ∖ {0})) | 
| 68 | 67 | eldifad 3962 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑗 ∈ dom 𝑑) | 
| 69 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑)) | 
| 70 | 69, 59 | wrdfd 32919 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑑:(0..^(♯‘𝑑))⟶𝐴) | 
| 71 | 70 | fdmd 6745 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → dom 𝑑 = (0..^(♯‘𝑑))) | 
| 72 | 68, 71 | eleqtrd 2842 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑗 ∈ (0..^(♯‘𝑑))) | 
| 73 | 66, 72 | sselid 3980 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑗 ∈ ℤ) | 
| 74 |  | eldifsni 4789 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (dom 𝑑 ∖ {0}) → 𝑗 ≠ 0) | 
| 75 | 67, 74 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑗 ≠ 0) | 
| 76 |  | fzo1fzo0n0 13755 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈
(1..^(♯‘𝑑))
↔ (𝑗 ∈
(0..^(♯‘𝑑))
∧ 𝑗 ≠
0)) | 
| 77 | 72, 75, 76 | sylanbrc 583 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑗 ∈ (1..^(♯‘𝑑))) | 
| 78 |  | elfzom1b 13806 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℤ ∧
(♯‘𝑑) ∈
ℤ) → (𝑗 ∈
(1..^(♯‘𝑑))
↔ (𝑗 − 1) ∈
(0..^((♯‘𝑑)
− 1)))) | 
| 79 | 78 | biimpa 476 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑗 ∈ ℤ ∧
(♯‘𝑑) ∈
ℤ) ∧ 𝑗 ∈
(1..^(♯‘𝑑)))
→ (𝑗 − 1) ∈
(0..^((♯‘𝑑)
− 1))) | 
| 80 | 73, 63, 77, 79 | syl21anc 837 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1))) | 
| 81 | 65, 80 | sseldd 3983 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (𝑗 − 1) ∈ (0..^(♯‘𝑑))) | 
| 82 |  | ccatval1 14616 | . . . . . . . . . . . . . . . 16
⊢ ((𝑑 ∈ Word 𝐴 ∧ 〈“𝑥”〉 ∈ Word 𝐴 ∧ (𝑗 − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ 〈“𝑥”〉)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1))) | 
| 83 | 59, 60, 81, 82 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ((𝑑 ++ 〈“𝑥”〉)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1))) | 
| 84 |  | ccatval1 14616 | . . . . . . . . . . . . . . . 16
⊢ ((𝑑 ∈ Word 𝐴 ∧ 〈“𝑥”〉 ∈ Word 𝐴 ∧ 𝑗 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) = (𝑑‘𝑗)) | 
| 85 | 59, 60, 72, 84 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) = (𝑑‘𝑗)) | 
| 86 | 58, 83, 85 | 3brtr3d 5173 | . . . . . . . . . . . . . 14
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)) | 
| 87 | 86 | an32s 652 | . . . . . . . . . . . . 13
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)) | 
| 88 | 87 | adantllr 719 | . . . . . . . . . . . 12
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)) | 
| 89 | 88 | ralrimiva 3145 | . . . . . . . . . . 11
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)) | 
| 90 | 89 | an32s 652 | . . . . . . . . . 10
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)) | 
| 91 |  | ischn 32997 | . . . . . . . . . 10
⊢ (𝑑 ∈ ( < Chain𝐴) ↔ (𝑑 ∈ Word 𝐴 ∧ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))) | 
| 92 | 46, 90, 91 | sylanbrc 583 | . . . . . . . . 9
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ ( < Chain𝐴)) | 
| 93 | 45, 92 | jca 511 | . . . . . . . 8
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → (𝜑 ∧ 𝑑 ∈ ( < Chain𝐴))) | 
| 94 |  | simp-4r 783 | . . . . . . . 8
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → 𝑥 ∈ 𝐴) | 
| 95 |  | lsw 14603 | . . . . . . . . . . . . 13
⊢ (𝑑 ∈ Word 𝐴 → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1))) | 
| 96 | 95 | ad5antr 734 | . . . . . . . . . . . 12
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1))) | 
| 97 |  | simp-4l 782 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ∈ Word 𝐴) | 
| 98 |  | fzonn0p1 13782 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑑)
∈ ℕ0 → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1))) | 
| 99 | 97, 61, 98 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1))) | 
| 100 |  | ccatws1len 14659 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ 〈“𝑥”〉)) = ((♯‘𝑑) + 1)) | 
| 101 | 100 | ad4antr 732 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘(𝑑 ++ 〈“𝑥”〉)) = ((♯‘𝑑) + 1)) | 
| 102 | 101 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ((♯‘𝑑) + 1) = (♯‘(𝑑 ++ 〈“𝑥”〉))) | 
| 103 |  | ccatws1cl 14655 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ++ 〈“𝑥”〉) ∈ Word 𝐴) | 
| 104 | 103 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ 〈“𝑥”〉) ∈ Word 𝐴) | 
| 105 | 102, 104 | wrdfd 32919 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ 〈“𝑥”〉):(0..^((♯‘𝑑) + 1))⟶𝐴) | 
| 106 | 105 | fdmd 6745 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → dom (𝑑 ++ 〈“𝑥”〉) = (0..^((♯‘𝑑) + 1))) | 
| 107 | 99, 106 | eleqtrrd 2843 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ dom (𝑑 ++ 〈“𝑥”〉)) | 
| 108 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ¬ 𝑑 = ∅) | 
| 109 | 108 | neqned 2946 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ≠ ∅) | 
| 110 |  | hasheq0 14403 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) = 0 ↔ 𝑑 = ∅)) | 
| 111 | 110 | necon3bid 2984 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) ≠ 0 ↔ 𝑑 ≠ ∅)) | 
| 112 | 111 | biimpar 477 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0) | 
| 113 | 97, 109, 112 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ≠ 0) | 
| 114 | 107, 113 | eldifsnd 4786 | . . . . . . . . . . . . . . 15
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})) | 
| 115 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) = ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1))) | 
| 116 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ 〈“𝑥”〉)‘𝑖) = ((𝑑 ++ 〈“𝑥”〉)‘(♯‘𝑑))) | 
| 117 | 115, 116 | breq12d 5155 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = (♯‘𝑑) → (((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖) ↔ ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘(♯‘𝑑)))) | 
| 118 | 117 | adantl 481 | . . . . . . . . . . . . . . 15
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ 𝑖 = (♯‘𝑑)) → (((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖) ↔ ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘(♯‘𝑑)))) | 
| 119 | 114, 118 | rspcdv 3613 | . . . . . . . . . . . . . 14
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖) → ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘(♯‘𝑑)))) | 
| 120 | 119 | imp 406 | . . . . . . . . . . . . 13
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘(♯‘𝑑))) | 
| 121 | 47 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑑 ∈ Word 𝐴) | 
| 122 | 49 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 〈“𝑥”〉 ∈ Word 𝐴) | 
| 123 | 121, 61 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (♯‘𝑑) ∈
ℕ0) | 
| 124 | 113 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (♯‘𝑑) ≠ 0) | 
| 125 |  | elnnne0 12542 | . . . . . . . . . . . . . . . 16
⊢
((♯‘𝑑)
∈ ℕ ↔ ((♯‘𝑑) ∈ ℕ0 ∧
(♯‘𝑑) ≠
0)) | 
| 126 | 123, 124,
125 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (♯‘𝑑) ∈ ℕ) | 
| 127 |  | fzo0end 13798 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝑑)
∈ ℕ → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) | 
| 128 | 126, 127 | syl 17 | . . . . . . . . . . . . . 14
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) | 
| 129 |  | ccatval1 14616 | . . . . . . . . . . . . . 14
⊢ ((𝑑 ∈ Word 𝐴 ∧ 〈“𝑥”〉 ∈ Word 𝐴 ∧ ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1))) | 
| 130 | 121, 122,
128, 129 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1))) | 
| 131 | 48 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝑥 ∈ 𝐴) | 
| 132 |  | eqidd 2737 | . . . . . . . . . . . . . 14
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑)) | 
| 133 |  | ccats1val2 14666 | . . . . . . . . . . . . . 14
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ (♯‘𝑑) = (♯‘𝑑)) → ((𝑑 ++ 〈“𝑥”〉)‘(♯‘𝑑)) = 𝑥) | 
| 134 | 121, 131,
132, 133 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ((𝑑 ++ 〈“𝑥”〉)‘(♯‘𝑑)) = 𝑥) | 
| 135 | 120, 130,
134 | 3brtr3d 5173 | . . . . . . . . . . . 12
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (𝑑‘((♯‘𝑑) − 1)) < 𝑥) | 
| 136 | 96, 135 | eqbrtrd 5164 | . . . . . . . . . . 11
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (lastS‘𝑑) < 𝑥) | 
| 137 | 136 | an42ds 32470 | . . . . . . . . . 10
⊢
((((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) ∧ ¬ 𝑑 = ∅) → (lastS‘𝑑) < 𝑥) | 
| 138 | 137 | ex 412 | . . . . . . . . 9
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → (¬ 𝑑 = ∅ → (lastS‘𝑑) < 𝑥)) | 
| 139 | 138 | orrd 863 | . . . . . . . 8
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) | 
| 140 |  | simpr 484 | . . . . . . . 8
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → 𝜃) | 
| 141 |  | chnind.8 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏) | 
| 142 | 93, 94, 139, 140, 141 | syl1111anc 840 | . . . . . . 7
⊢
(((((𝑑 ∈ Word
𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) ∧ 𝜃) → 𝜏) | 
| 143 | 142 | ex 412 | . . . . . 6
⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (𝜃 → 𝜏)) | 
| 144 | 143 | expl 457 | . . . . 5
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → (𝜃 → 𝜏))) | 
| 145 | 87 | ralrimiva 3145 | . . . . . . 7
⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)) | 
| 146 |  | fvoveq1 7455 | . . . . . . . . 9
⊢ (𝑖 = 𝑗 → (𝑑‘(𝑖 − 1)) = (𝑑‘(𝑗 − 1))) | 
| 147 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑖 = 𝑗 → (𝑑‘𝑖) = (𝑑‘𝑗)) | 
| 148 | 146, 147 | breq12d 5155 | . . . . . . . 8
⊢ (𝑖 = 𝑗 → ((𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))) | 
| 149 | 148 | cbvralvw 3236 | . . . . . . 7
⊢
(∀𝑖 ∈
(dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)) | 
| 150 | 145, 149 | sylibr 234 | . . . . . 6
⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) | 
| 151 | 150 | expl 457 | . . . . 5
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))) | 
| 152 | 144, 151 | a2and 845 | . . . 4
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ 〈“𝑥”〉) ∖ {0})((𝑑 ++ 〈“𝑥”〉)‘(𝑖 − 1)) < ((𝑑 ++ 〈“𝑥”〉)‘𝑖)) → 𝜏))) | 
| 153 | 15, 24, 33, 42, 44, 152 | wrdind 14761 | . . 3
⊢ (𝐶 ∈ Word 𝐴 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂)) | 
| 154 | 153 | imp 406 | . 2
⊢ ((𝐶 ∈ Word 𝐴 ∧ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) → 𝜂) | 
| 155 | 2, 3, 6, 154 | syl12anc 836 | 1
⊢ (𝜑 → 𝜂) |