| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . 3
⊢ (𝑖 = 𝐼 → (𝐶‘𝑖) = (𝐶‘𝐼)) |
| 2 | 1 | breq1d 5153 |
. 2
⊢ (𝑖 = 𝐼 → ((𝐶‘𝑖) < (lastS‘𝐶) ↔ (𝐶‘𝐼) < (lastS‘𝐶))) |
| 3 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = ∅ →
(♯‘𝑐) =
(♯‘∅)) |
| 4 | 3 | oveq1d 7446 |
. . . . 5
⊢ (𝑐 = ∅ →
((♯‘𝑐) −
1) = ((♯‘∅) − 1)) |
| 5 | 4 | oveq2d 7447 |
. . . 4
⊢ (𝑐 = ∅ →
(0..^((♯‘𝑐)
− 1)) = (0..^((♯‘∅) − 1))) |
| 6 | | fveq1 6905 |
. . . . 5
⊢ (𝑐 = ∅ → (𝑐‘𝑖) = (∅‘𝑖)) |
| 7 | | fveq2 6906 |
. . . . 5
⊢ (𝑐 = ∅ →
(lastS‘𝑐) =
(lastS‘∅)) |
| 8 | 6, 7 | breq12d 5156 |
. . . 4
⊢ (𝑐 = ∅ → ((𝑐‘𝑖) < (lastS‘𝑐) ↔ (∅‘𝑖) <
(lastS‘∅))) |
| 9 | 5, 8 | raleqbidv 3346 |
. . 3
⊢ (𝑐 = ∅ → (∀𝑖 ∈
(0..^((♯‘𝑐)
− 1))(𝑐‘𝑖) < (lastS‘𝑐) ↔ ∀𝑖 ∈
(0..^((♯‘∅) − 1))(∅‘𝑖) <
(lastS‘∅))) |
| 10 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = 𝑑 → (♯‘𝑐) = (♯‘𝑑)) |
| 11 | 10 | oveq1d 7446 |
. . . . 5
⊢ (𝑐 = 𝑑 → ((♯‘𝑐) − 1) = ((♯‘𝑑) − 1)) |
| 12 | 11 | oveq2d 7447 |
. . . 4
⊢ (𝑐 = 𝑑 → (0..^((♯‘𝑐) − 1)) =
(0..^((♯‘𝑑)
− 1))) |
| 13 | | fveq1 6905 |
. . . . 5
⊢ (𝑐 = 𝑑 → (𝑐‘𝑖) = (𝑑‘𝑖)) |
| 14 | | fveq2 6906 |
. . . . 5
⊢ (𝑐 = 𝑑 → (lastS‘𝑐) = (lastS‘𝑑)) |
| 15 | 13, 14 | breq12d 5156 |
. . . 4
⊢ (𝑐 = 𝑑 → ((𝑐‘𝑖) < (lastS‘𝑐) ↔ (𝑑‘𝑖) < (lastS‘𝑑))) |
| 16 | 12, 15 | raleqbidv 3346 |
. . 3
⊢ (𝑐 = 𝑑 → (∀𝑖 ∈ (0..^((♯‘𝑐) − 1))(𝑐‘𝑖) < (lastS‘𝑐) ↔ ∀𝑖 ∈
(0..^((♯‘𝑑)
− 1))(𝑑‘𝑖) < (lastS‘𝑑))) |
| 17 | | fveq2 6906 |
. . . . . 6
⊢ (𝑖 = 𝑗 → (𝑐‘𝑖) = (𝑐‘𝑗)) |
| 18 | 17 | breq1d 5153 |
. . . . 5
⊢ (𝑖 = 𝑗 → ((𝑐‘𝑖) < (lastS‘𝑐) ↔ (𝑐‘𝑗) < (lastS‘𝑐))) |
| 19 | 18 | cbvralvw 3237 |
. . . 4
⊢
(∀𝑖 ∈
(0..^((♯‘𝑐)
− 1))(𝑐‘𝑖) < (lastS‘𝑐) ↔ ∀𝑗 ∈
(0..^((♯‘𝑐)
− 1))(𝑐‘𝑗) < (lastS‘𝑐)) |
| 20 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (♯‘𝑐) = (♯‘(𝑑 ++ 〈“𝑥”〉))) |
| 21 | 20 | oveq1d 7446 |
. . . . . 6
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → ((♯‘𝑐) − 1) =
((♯‘(𝑑 ++
〈“𝑥”〉)) − 1)) |
| 22 | 21 | oveq2d 7447 |
. . . . 5
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) →
(0..^((♯‘𝑐)
− 1)) = (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1))) |
| 23 | | fveq1 6905 |
. . . . . 6
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (𝑐‘𝑗) = ((𝑑 ++ 〈“𝑥”〉)‘𝑗)) |
| 24 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (lastS‘𝑐) = (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 25 | 23, 24 | breq12d 5156 |
. . . . 5
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → ((𝑐‘𝑗) < (lastS‘𝑐) ↔ ((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉)))) |
| 26 | 22, 25 | raleqbidv 3346 |
. . . 4
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (∀𝑗 ∈
(0..^((♯‘𝑐)
− 1))(𝑐‘𝑗) < (lastS‘𝑐) ↔ ∀𝑗 ∈
(0..^((♯‘(𝑑 ++
〈“𝑥”〉)) − 1))((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉)))) |
| 27 | 19, 26 | bitrid 283 |
. . 3
⊢ (𝑐 = (𝑑 ++ 〈“𝑥”〉) → (∀𝑖 ∈
(0..^((♯‘𝑐)
− 1))(𝑐‘𝑖) < (lastS‘𝑐) ↔ ∀𝑗 ∈
(0..^((♯‘(𝑑 ++
〈“𝑥”〉)) − 1))((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉)))) |
| 28 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (♯‘𝑐) = (♯‘𝐶)) |
| 29 | 28 | oveq1d 7446 |
. . . . 5
⊢ (𝑐 = 𝐶 → ((♯‘𝑐) − 1) = ((♯‘𝐶) − 1)) |
| 30 | 29 | oveq2d 7447 |
. . . 4
⊢ (𝑐 = 𝐶 → (0..^((♯‘𝑐) − 1)) =
(0..^((♯‘𝐶)
− 1))) |
| 31 | | fveq1 6905 |
. . . . 5
⊢ (𝑐 = 𝐶 → (𝑐‘𝑖) = (𝐶‘𝑖)) |
| 32 | | fveq2 6906 |
. . . . 5
⊢ (𝑐 = 𝐶 → (lastS‘𝑐) = (lastS‘𝐶)) |
| 33 | 31, 32 | breq12d 5156 |
. . . 4
⊢ (𝑐 = 𝐶 → ((𝑐‘𝑖) < (lastS‘𝑐) ↔ (𝐶‘𝑖) < (lastS‘𝐶))) |
| 34 | 30, 33 | raleqbidv 3346 |
. . 3
⊢ (𝑐 = 𝐶 → (∀𝑖 ∈ (0..^((♯‘𝑐) − 1))(𝑐‘𝑖) < (lastS‘𝑐) ↔ ∀𝑖 ∈
(0..^((♯‘𝐶)
− 1))(𝐶‘𝑖) < (lastS‘𝐶))) |
| 35 | | chnub.2 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) |
| 36 | | ral0 4513 |
. . . . 5
⊢
∀𝑖 ∈
∅ (∅‘𝑖)
<
(lastS‘∅) |
| 37 | | hash0 14406 |
. . . . . . . . 9
⊢
(♯‘∅) = 0 |
| 38 | 37 | oveq1i 7441 |
. . . . . . . 8
⊢
((♯‘∅) − 1) = (0 − 1) |
| 39 | | df-neg 11495 |
. . . . . . . . 9
⊢ -1 = (0
− 1) |
| 40 | | neg1rr 12381 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
| 41 | | 0re 11263 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
| 42 | | neg1lt0 12383 |
. . . . . . . . . 10
⊢ -1 <
0 |
| 43 | 40, 41, 42 | ltleii 11384 |
. . . . . . . . 9
⊢ -1 ≤
0 |
| 44 | 39, 43 | eqbrtrri 5166 |
. . . . . . . 8
⊢ (0
− 1) ≤ 0 |
| 45 | 38, 44 | eqbrtri 5164 |
. . . . . . 7
⊢
((♯‘∅) − 1) ≤ 0 |
| 46 | | 0z 12624 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
| 47 | 37, 46 | eqeltri 2837 |
. . . . . . . . 9
⊢
(♯‘∅) ∈ ℤ |
| 48 | | 1z 12647 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
| 49 | | zsubcl 12659 |
. . . . . . . . 9
⊢
(((♯‘∅) ∈ ℤ ∧ 1 ∈ ℤ) →
((♯‘∅) − 1) ∈ ℤ) |
| 50 | 47, 48, 49 | mp2an 692 |
. . . . . . . 8
⊢
((♯‘∅) − 1) ∈ ℤ |
| 51 | | fzon 13720 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ ((♯‘∅) − 1) ∈ ℤ) →
(((♯‘∅) − 1) ≤ 0 ↔
(0..^((♯‘∅) − 1)) = ∅)) |
| 52 | 46, 50, 51 | mp2an 692 |
. . . . . . 7
⊢
(((♯‘∅) − 1) ≤ 0 ↔
(0..^((♯‘∅) − 1)) = ∅) |
| 53 | 45, 52 | mpbi 230 |
. . . . . 6
⊢
(0..^((♯‘∅) − 1)) = ∅ |
| 54 | 53 | raleqi 3324 |
. . . . 5
⊢
(∀𝑖 ∈
(0..^((♯‘∅) − 1))(∅‘𝑖) < (lastS‘∅)
↔ ∀𝑖 ∈
∅ (∅‘𝑖)
<
(lastS‘∅)) |
| 55 | 36, 54 | mpbir 231 |
. . . 4
⊢
∀𝑖 ∈
(0..^((♯‘∅) − 1))(∅‘𝑖) <
(lastS‘∅) |
| 56 | 55 | a1i 11 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ (0..^((♯‘∅) −
1))(∅‘𝑖) <
(lastS‘∅)) |
| 57 | | simp-6r 788 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
𝑑 ∈ ( < Chain𝐴)) |
| 58 | 57 | chnwrd 32997 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
𝑑 ∈ Word 𝐴) |
| 59 | | ccatws1len 14658 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ 〈“𝑥”〉)) = ((♯‘𝑑) + 1)) |
| 60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
(♯‘(𝑑 ++
〈“𝑥”〉)) = ((♯‘𝑑) + 1)) |
| 61 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
𝑑 =
∅) |
| 62 | 61 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
(♯‘𝑑) =
(♯‘∅)) |
| 63 | 62, 37 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
(♯‘𝑑) =
0) |
| 64 | 63 | oveq1d 7446 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
((♯‘𝑑) + 1) =
(0 + 1)) |
| 65 | | 0p1e1 12388 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
| 66 | 65 | a1i 11 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
(0 + 1) = 1) |
| 67 | 60, 64, 66 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
(♯‘(𝑑 ++
〈“𝑥”〉)) = 1) |
| 68 | 67 | oveq1d 7446 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
((♯‘(𝑑 ++
〈“𝑥”〉)) − 1) = (1 −
1)) |
| 69 | | 1m1e0 12338 |
. . . . . . . . 9
⊢ (1
− 1) = 0 |
| 70 | 68, 69 | eqtrdi 2793 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
((♯‘(𝑑 ++
〈“𝑥”〉)) − 1) =
0) |
| 71 | 70 | oveq2d 7447 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
(0..^((♯‘(𝑑 ++
〈“𝑥”〉)) − 1)) =
(0..^0)) |
| 72 | | fzo0 13723 |
. . . . . . 7
⊢ (0..^0) =
∅ |
| 73 | 71, 72 | eqtrdi 2793 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
(0..^((♯‘(𝑑 ++
〈“𝑥”〉)) − 1)) =
∅) |
| 74 | | simplr 769 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
𝑗 ∈
(0..^((♯‘(𝑑 ++
〈“𝑥”〉)) − 1))) |
| 75 | 74 | ne0d 4342 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
(0..^((♯‘(𝑑 ++
〈“𝑥”〉)) − 1)) ≠
∅) |
| 76 | 73, 75 | pm2.21ddne 3026 |
. . . . 5
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 = ∅) →
((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 77 | | chnub.1 |
. . . . . . . 8
⊢ (𝜑 → < Po 𝐴) |
| 78 | 77 | ad7antr 738 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → < Po 𝐴) |
| 79 | | simp-6r 788 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 𝑑 ∈ ( < Chain𝐴)) |
| 80 | 79 | chnwrd 32997 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 𝑑 ∈ Word 𝐴) |
| 81 | 80 | adantr 480 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → 𝑑
∈ Word 𝐴) |
| 82 | | simp-5r 786 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 𝑥 ∈ 𝐴) |
| 83 | 82 | adantr 480 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → 𝑥
∈ 𝐴) |
| 84 | | ccatws1cl 14654 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ++ 〈“𝑥”〉) ∈ Word 𝐴) |
| 85 | 81, 83, 84 | syl2anc 584 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (𝑑 ++
〈“𝑥”〉) ∈ Word 𝐴) |
| 86 | | lencl 14571 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈
ℕ0) |
| 87 | 80, 86 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (♯‘𝑑)
∈ ℕ0) |
| 88 | 87 | nn0zd 12639 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (♯‘𝑑)
∈ ℤ) |
| 89 | | 1zzd 12648 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 1 ∈ ℤ) |
| 90 | 88, 89 | zsubcld 12727 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘𝑑)
− 1) ∈ ℤ) |
| 91 | 88 | peano2zd 12725 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘𝑑) +
1) ∈ ℤ) |
| 92 | 90 | zred 12722 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘𝑑)
− 1) ∈ ℝ) |
| 93 | 91 | zred 12722 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘𝑑) +
1) ∈ ℝ) |
| 94 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 𝑑 ≠
∅) |
| 95 | | hasheq0 14402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) = 0 ↔ 𝑑 = ∅)) |
| 96 | 95 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) ≠ 0 ↔ 𝑑 ≠ ∅)) |
| 97 | 96 | biimpar 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0) |
| 98 | 80, 94, 97 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (♯‘𝑑)
≠ 0) |
| 99 | | elnnne0 12540 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑑)
∈ ℕ ↔ ((♯‘𝑑) ∈ ℕ0 ∧
(♯‘𝑑) ≠
0)) |
| 100 | 87, 98, 99 | sylanbrc 583 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (♯‘𝑑)
∈ ℕ) |
| 101 | 100 | nnred 12281 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (♯‘𝑑)
∈ ℝ) |
| 102 | 101 | ltm1d 12200 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘𝑑)
− 1) < (♯‘𝑑)) |
| 103 | 101 | ltp1d 12198 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (♯‘𝑑)
< ((♯‘𝑑) +
1)) |
| 104 | 92, 101, 93, 102, 103 | lttrd 11422 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘𝑑)
− 1) < ((♯‘𝑑) + 1)) |
| 105 | 92, 93, 104 | ltled 11409 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘𝑑)
− 1) ≤ ((♯‘𝑑) + 1)) |
| 106 | | eluz2 12884 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑑)
+ 1) ∈ (ℤ≥‘((♯‘𝑑) − 1)) ↔ (((♯‘𝑑) − 1) ∈ ℤ
∧ ((♯‘𝑑) +
1) ∈ ℤ ∧ ((♯‘𝑑) − 1) ≤ ((♯‘𝑑) + 1))) |
| 107 | 90, 91, 105, 106 | syl3anbrc 1344 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘𝑑) +
1) ∈ (ℤ≥‘((♯‘𝑑) − 1))) |
| 108 | | fzoss2 13727 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑑)
+ 1) ∈ (ℤ≥‘((♯‘𝑑) − 1)) →
(0..^((♯‘𝑑)
− 1)) ⊆ (0..^((♯‘𝑑) + 1))) |
| 109 | 107, 108 | syl 17 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (0..^((♯‘𝑑) − 1)) ⊆
(0..^((♯‘𝑑) +
1))) |
| 110 | 109 | sselda 3983 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → 𝑗
∈ (0..^((♯‘𝑑) + 1))) |
| 111 | 81, 59 | syl 17 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (♯‘(𝑑 ++ 〈“𝑥”〉)) = ((♯‘𝑑) + 1)) |
| 112 | 111 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (0..^(♯‘(𝑑 ++ 〈“𝑥”〉))) = (0..^((♯‘𝑑) + 1))) |
| 113 | 110, 112 | eleqtrrd 2844 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → 𝑗
∈ (0..^(♯‘(𝑑 ++ 〈“𝑥”〉)))) |
| 114 | | wrdsymbcl 14565 |
. . . . . . . . 9
⊢ (((𝑑 ++ 〈“𝑥”〉) ∈ Word 𝐴 ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ 〈“𝑥”〉)))) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) ∈ 𝐴) |
| 115 | 85, 113, 114 | syl2anc 584 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → ((𝑑 ++
〈“𝑥”〉)‘𝑗) ∈ 𝐴) |
| 116 | | simplr 769 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → 𝑑 ≠
∅) |
| 117 | | lswcl 14606 |
. . . . . . . . 9
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅) → (lastS‘𝑑) ∈ 𝐴) |
| 118 | 81, 116, 117 | syl2anc 584 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (lastS‘𝑑) ∈ 𝐴) |
| 119 | | lswccats1 14672 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (lastS‘(𝑑 ++ 〈“𝑥”〉)) = 𝑥) |
| 120 | 80, 82, 119 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (lastS‘(𝑑 ++
〈“𝑥”〉)) = 𝑥) |
| 121 | 120 | adantr 480 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (lastS‘(𝑑 ++ 〈“𝑥”〉)) = 𝑥) |
| 122 | 121, 83 | eqeltrd 2841 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (lastS‘(𝑑 ++ 〈“𝑥”〉)) ∈ 𝐴) |
| 123 | 115, 118,
122 | 3jca 1129 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (((𝑑 ++
〈“𝑥”〉)‘𝑗) ∈ 𝐴 ∧ (lastS‘𝑑) ∈ 𝐴 ∧ (lastS‘(𝑑 ++ 〈“𝑥”〉)) ∈ 𝐴)) |
| 124 | | simplr 769 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 𝑗 ∈
(0..^((♯‘(𝑑 ++
〈“𝑥”〉)) − 1))) |
| 125 | 59 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ Word 𝐴 → ((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1) =
(((♯‘𝑑) + 1)
− 1)) |
| 126 | 80, 125 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘(𝑑
++ 〈“𝑥”〉)) − 1) =
(((♯‘𝑑) + 1)
− 1)) |
| 127 | 100 | nncnd 12282 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (♯‘𝑑)
∈ ℂ) |
| 128 | | 1cnd 11256 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 1 ∈ ℂ) |
| 129 | 127, 128 | pncand 11621 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (((♯‘𝑑)
+ 1) − 1) = (♯‘𝑑)) |
| 130 | 126, 129 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((♯‘(𝑑
++ 〈“𝑥”〉)) − 1) =
(♯‘𝑑)) |
| 131 | 130 | oveq2d 7447 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)) =
(0..^(♯‘𝑑))) |
| 132 | 124, 131 | eleqtrd 2843 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 𝑗 ∈
(0..^(♯‘𝑑))) |
| 133 | 132 | adantr 480 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → 𝑗
∈ (0..^(♯‘𝑑))) |
| 134 | | ccats1val1 14664 |
. . . . . . . . 9
⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑗 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) = (𝑑‘𝑗)) |
| 135 | 81, 133, 134 | syl2anc 584 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → ((𝑑 ++
〈“𝑥”〉)‘𝑗) = (𝑑‘𝑗)) |
| 136 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑑‘𝑖) = (𝑑‘𝑗)) |
| 137 | 136 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((𝑑‘𝑖) < (lastS‘𝑑) ↔ (𝑑‘𝑗) < (lastS‘𝑑))) |
| 138 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) |
| 139 | | simpr 484 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → 𝑗
∈ (0..^((♯‘𝑑) − 1))) |
| 140 | 137, 138,
139 | rspcdva 3623 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (𝑑‘𝑗) < (lastS‘𝑑)) |
| 141 | 135, 140 | eqbrtrd 5165 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → ((𝑑 ++
〈“𝑥”〉)‘𝑗) < (lastS‘𝑑)) |
| 142 | | simp-4r 784 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (𝑑 = ∅ ∨
(lastS‘𝑑) < 𝑥)) |
| 143 | 94 | neneqd 2945 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ¬ 𝑑 =
∅) |
| 144 | 142, 143 | orcnd 879 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (lastS‘𝑑)
<
𝑥) |
| 145 | 144 | adantr 480 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (lastS‘𝑑) < 𝑥) |
| 146 | 145, 121 | breqtrrd 5171 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → (lastS‘𝑑) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 147 | | potr 5605 |
. . . . . . . 8
⊢ (( < Po 𝐴 ∧ (((𝑑 ++ 〈“𝑥”〉)‘𝑗) ∈ 𝐴 ∧ (lastS‘𝑑) ∈ 𝐴 ∧ (lastS‘(𝑑 ++ 〈“𝑥”〉)) ∈ 𝐴)) → ((((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘𝑑) ∧ (lastS‘𝑑) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉)))) |
| 148 | 147 | imp 406 |
. . . . . . 7
⊢ ((( < Po 𝐴 ∧ (((𝑑 ++ 〈“𝑥”〉)‘𝑗) ∈ 𝐴 ∧ (lastS‘𝑑) ∈ 𝐴 ∧ (lastS‘(𝑑 ++ 〈“𝑥”〉)) ∈ 𝐴)) ∧ (((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘𝑑) ∧ (lastS‘𝑑) < (lastS‘(𝑑 ++ 〈“𝑥”〉)))) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 149 | 78, 123, 141, 146, 148 | syl22anc 839 |
. . . . . 6
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 ∈
(0..^((♯‘𝑑)
− 1))) → ((𝑑 ++
〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 150 | 144 | adantr 480 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) →
(lastS‘𝑑) < 𝑥) |
| 151 | 80 | adantr 480 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) → 𝑑 ∈ Word 𝐴) |
| 152 | | simp-6r 788 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) → 𝑥 ∈ 𝐴) |
| 153 | 152 | s1cld 14641 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) →
〈“𝑥”〉
∈ Word 𝐴) |
| 154 | 100 | adantr 480 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) →
(♯‘𝑑) ∈
ℕ) |
| 155 | | fzo0end 13797 |
. . . . . . . . . 10
⊢
((♯‘𝑑)
∈ ℕ → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) |
| 156 | 154, 155 | syl 17 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) →
((♯‘𝑑) −
1) ∈ (0..^(♯‘𝑑))) |
| 157 | | ccatval1 14615 |
. . . . . . . . 9
⊢ ((𝑑 ∈ Word 𝐴 ∧ 〈“𝑥”〉 ∈ Word 𝐴 ∧ ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1))) |
| 158 | 151, 153,
156, 157 | syl3anc 1373 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) → ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1))) |
| 159 | | simpr 484 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) → 𝑗 = ((♯‘𝑑) − 1)) |
| 160 | 159 | fveq2d 6910 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) = ((𝑑 ++ 〈“𝑥”〉)‘((♯‘𝑑) − 1))) |
| 161 | | lsw 14602 |
. . . . . . . . 9
⊢ (𝑑 ∈ Word 𝐴 → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1))) |
| 162 | 151, 161 | syl 17 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) →
(lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1))) |
| 163 | 158, 160,
162 | 3eqtr4d 2787 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) = (lastS‘𝑑)) |
| 164 | 120 | adantr 480 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) →
(lastS‘(𝑑 ++
〈“𝑥”〉)) = 𝑥) |
| 165 | 150, 163,
164 | 3brtr4d 5175 |
. . . . . 6
⊢
((((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅) ∧
𝑗 = ((♯‘𝑑) − 1)) → ((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 166 | 65 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(ℤ≥‘(0 + 1)) =
(ℤ≥‘1) |
| 167 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 168 | 166, 167 | eqtr4i 2768 |
. . . . . . . . . 10
⊢
(ℤ≥‘(0 + 1)) = ℕ |
| 169 | 100, 168 | eleqtrrdi 2852 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (♯‘𝑑)
∈ (ℤ≥‘(0 + 1))) |
| 170 | | fzosplitsnm1 13779 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ (♯‘𝑑) ∈ (ℤ≥‘(0 +
1))) → (0..^(♯‘𝑑)) = ((0..^((♯‘𝑑) − 1)) ∪ {((♯‘𝑑) − 1)})) |
| 171 | 46, 169, 170 | sylancr 587 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (0..^(♯‘𝑑)) = ((0..^((♯‘𝑑) − 1)) ∪ {((♯‘𝑑) − 1)})) |
| 172 | 132, 171 | eleqtrd 2843 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ 𝑗 ∈
((0..^((♯‘𝑑)
− 1)) ∪ {((♯‘𝑑) − 1)})) |
| 173 | | elunsn 4683 |
. . . . . . . 8
⊢ (𝑗 ∈
((0..^((♯‘𝑑)
− 1)) ∪ {((♯‘𝑑) − 1)}) → (𝑗 ∈ ((0..^((♯‘𝑑) − 1)) ∪
{((♯‘𝑑) −
1)}) ↔ (𝑗 ∈
(0..^((♯‘𝑑)
− 1)) ∨ 𝑗 =
((♯‘𝑑) −
1)))) |
| 174 | 173 | ibi 267 |
. . . . . . 7
⊢ (𝑗 ∈
((0..^((♯‘𝑑)
− 1)) ∪ {((♯‘𝑑) − 1)}) → (𝑗 ∈ (0..^((♯‘𝑑) − 1)) ∨ 𝑗 = ((♯‘𝑑) − 1))) |
| 175 | 172, 174 | syl 17 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ (𝑗 ∈
(0..^((♯‘𝑑)
− 1)) ∨ 𝑗 =
((♯‘𝑑) −
1))) |
| 176 | 149, 165,
175 | mpjaodan 961 |
. . . . 5
⊢
(((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
∧ 𝑑 ≠ ∅)
→ ((𝑑 ++
〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 177 | 76, 176 | pm2.61dane 3029 |
. . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ 〈“𝑥”〉)) − 1)))
→ ((𝑑 ++
〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 178 | 177 | ralrimiva 3146 |
. . 3
⊢
(((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑‘𝑖) < (lastS‘𝑑)) → ∀𝑗 ∈
(0..^((♯‘(𝑑 ++
〈“𝑥”〉)) − 1))((𝑑 ++ 〈“𝑥”〉)‘𝑗) < (lastS‘(𝑑 ++ 〈“𝑥”〉))) |
| 179 | 9, 16, 27, 34, 35, 56, 178 | chnind 33001 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ (0..^((♯‘𝐶) − 1))(𝐶‘𝑖) < (lastS‘𝐶)) |
| 180 | | chnub.3 |
. 2
⊢ (𝜑 → 𝐼 ∈ (0..^((♯‘𝐶) − 1))) |
| 181 | 2, 179, 180 | rspcdva 3623 |
1
⊢ (𝜑 → (𝐶‘𝐼) < (lastS‘𝐶)) |