Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  chnub Structured version   Visualization version   GIF version

Theorem chnub 32985
Description: In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025.)
Hypotheses
Ref Expression
chnub.1 (𝜑< Po 𝐴)
chnub.2 (𝜑𝐶 ∈ ( < Chain𝐴))
chnub.3 (𝜑𝐼 ∈ (0..^((♯‘𝐶) − 1)))
Assertion
Ref Expression
chnub (𝜑 → (𝐶𝐼) < (lastS‘𝐶))

Proof of Theorem chnub
Dummy variables 𝑐 𝑑 𝑥 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6906 . . 3 (𝑖 = 𝐼 → (𝐶𝑖) = (𝐶𝐼))
21breq1d 5157 . 2 (𝑖 = 𝐼 → ((𝐶𝑖) < (lastS‘𝐶) ↔ (𝐶𝐼) < (lastS‘𝐶)))
3 fveq2 6906 . . . . . 6 (𝑐 = ∅ → (♯‘𝑐) = (♯‘∅))
43oveq1d 7445 . . . . 5 (𝑐 = ∅ → ((♯‘𝑐) − 1) = ((♯‘∅) − 1))
54oveq2d 7446 . . . 4 (𝑐 = ∅ → (0..^((♯‘𝑐) − 1)) = (0..^((♯‘∅) − 1)))
6 fveq1 6905 . . . . 5 (𝑐 = ∅ → (𝑐𝑖) = (∅‘𝑖))
7 fveq2 6906 . . . . 5 (𝑐 = ∅ → (lastS‘𝑐) = (lastS‘∅))
86, 7breq12d 5160 . . . 4 (𝑐 = ∅ → ((𝑐𝑖) < (lastS‘𝑐) ↔ (∅‘𝑖) < (lastS‘∅)))
95, 8raleqbidv 3343 . . 3 (𝑐 = ∅ → (∀𝑖 ∈ (0..^((♯‘𝑐) − 1))(𝑐𝑖) < (lastS‘𝑐) ↔ ∀𝑖 ∈ (0..^((♯‘∅) − 1))(∅‘𝑖) < (lastS‘∅)))
10 fveq2 6906 . . . . . 6 (𝑐 = 𝑑 → (♯‘𝑐) = (♯‘𝑑))
1110oveq1d 7445 . . . . 5 (𝑐 = 𝑑 → ((♯‘𝑐) − 1) = ((♯‘𝑑) − 1))
1211oveq2d 7446 . . . 4 (𝑐 = 𝑑 → (0..^((♯‘𝑐) − 1)) = (0..^((♯‘𝑑) − 1)))
13 fveq1 6905 . . . . 5 (𝑐 = 𝑑 → (𝑐𝑖) = (𝑑𝑖))
14 fveq2 6906 . . . . 5 (𝑐 = 𝑑 → (lastS‘𝑐) = (lastS‘𝑑))
1513, 14breq12d 5160 . . . 4 (𝑐 = 𝑑 → ((𝑐𝑖) < (lastS‘𝑐) ↔ (𝑑𝑖) < (lastS‘𝑑)))
1612, 15raleqbidv 3343 . . 3 (𝑐 = 𝑑 → (∀𝑖 ∈ (0..^((♯‘𝑐) − 1))(𝑐𝑖) < (lastS‘𝑐) ↔ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)))
17 fveq2 6906 . . . . . 6 (𝑖 = 𝑗 → (𝑐𝑖) = (𝑐𝑗))
1817breq1d 5157 . . . . 5 (𝑖 = 𝑗 → ((𝑐𝑖) < (lastS‘𝑐) ↔ (𝑐𝑗) < (lastS‘𝑐)))
1918cbvralvw 3234 . . . 4 (∀𝑖 ∈ (0..^((♯‘𝑐) − 1))(𝑐𝑖) < (lastS‘𝑐) ↔ ∀𝑗 ∈ (0..^((♯‘𝑐) − 1))(𝑐𝑗) < (lastS‘𝑐))
20 fveq2 6906 . . . . . . 7 (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (♯‘𝑐) = (♯‘(𝑑 ++ ⟨“𝑥”⟩)))
2120oveq1d 7445 . . . . . 6 (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((♯‘𝑐) − 1) = ((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))
2221oveq2d 7446 . . . . 5 (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (0..^((♯‘𝑐) − 1)) = (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1)))
23 fveq1 6905 . . . . . 6 (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐𝑗) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
24 fveq2 6906 . . . . . 6 (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (lastS‘𝑐) = (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
2523, 24breq12d 5160 . . . . 5 (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝑐𝑗) < (lastS‘𝑐) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩))))
2622, 25raleqbidv 3343 . . . 4 (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑗 ∈ (0..^((♯‘𝑐) − 1))(𝑐𝑗) < (lastS‘𝑐) ↔ ∀𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩))))
2719, 26bitrid 283 . . 3 (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑖 ∈ (0..^((♯‘𝑐) − 1))(𝑐𝑖) < (lastS‘𝑐) ↔ ∀𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩))))
28 fveq2 6906 . . . . . 6 (𝑐 = 𝐶 → (♯‘𝑐) = (♯‘𝐶))
2928oveq1d 7445 . . . . 5 (𝑐 = 𝐶 → ((♯‘𝑐) − 1) = ((♯‘𝐶) − 1))
3029oveq2d 7446 . . . 4 (𝑐 = 𝐶 → (0..^((♯‘𝑐) − 1)) = (0..^((♯‘𝐶) − 1)))
31 fveq1 6905 . . . . 5 (𝑐 = 𝐶 → (𝑐𝑖) = (𝐶𝑖))
32 fveq2 6906 . . . . 5 (𝑐 = 𝐶 → (lastS‘𝑐) = (lastS‘𝐶))
3331, 32breq12d 5160 . . . 4 (𝑐 = 𝐶 → ((𝑐𝑖) < (lastS‘𝑐) ↔ (𝐶𝑖) < (lastS‘𝐶)))
3430, 33raleqbidv 3343 . . 3 (𝑐 = 𝐶 → (∀𝑖 ∈ (0..^((♯‘𝑐) − 1))(𝑐𝑖) < (lastS‘𝑐) ↔ ∀𝑖 ∈ (0..^((♯‘𝐶) − 1))(𝐶𝑖) < (lastS‘𝐶)))
35 chnub.2 . . 3 (𝜑𝐶 ∈ ( < Chain𝐴))
36 ral0 4518 . . . . 5 𝑖 ∈ ∅ (∅‘𝑖) < (lastS‘∅)
37 hash0 14402 . . . . . . . . 9 (♯‘∅) = 0
3837oveq1i 7440 . . . . . . . 8 ((♯‘∅) − 1) = (0 − 1)
39 df-neg 11492 . . . . . . . . 9 -1 = (0 − 1)
40 neg1rr 12378 . . . . . . . . . 10 -1 ∈ ℝ
41 0re 11260 . . . . . . . . . 10 0 ∈ ℝ
42 neg1lt0 12380 . . . . . . . . . 10 -1 < 0
4340, 41, 42ltleii 11381 . . . . . . . . 9 -1 ≤ 0
4439, 43eqbrtrri 5170 . . . . . . . 8 (0 − 1) ≤ 0
4538, 44eqbrtri 5168 . . . . . . 7 ((♯‘∅) − 1) ≤ 0
46 0z 12621 . . . . . . . 8 0 ∈ ℤ
4737, 46eqeltri 2834 . . . . . . . . 9 (♯‘∅) ∈ ℤ
48 1z 12644 . . . . . . . . 9 1 ∈ ℤ
49 zsubcl 12656 . . . . . . . . 9 (((♯‘∅) ∈ ℤ ∧ 1 ∈ ℤ) → ((♯‘∅) − 1) ∈ ℤ)
5047, 48, 49mp2an 692 . . . . . . . 8 ((♯‘∅) − 1) ∈ ℤ
51 fzon 13716 . . . . . . . 8 ((0 ∈ ℤ ∧ ((♯‘∅) − 1) ∈ ℤ) → (((♯‘∅) − 1) ≤ 0 ↔ (0..^((♯‘∅) − 1)) = ∅))
5246, 50, 51mp2an 692 . . . . . . 7 (((♯‘∅) − 1) ≤ 0 ↔ (0..^((♯‘∅) − 1)) = ∅)
5345, 52mpbi 230 . . . . . 6 (0..^((♯‘∅) − 1)) = ∅
5453raleqi 3321 . . . . 5 (∀𝑖 ∈ (0..^((♯‘∅) − 1))(∅‘𝑖) < (lastS‘∅) ↔ ∀𝑖 ∈ ∅ (∅‘𝑖) < (lastS‘∅))
5536, 54mpbir 231 . . . 4 𝑖 ∈ (0..^((♯‘∅) − 1))(∅‘𝑖) < (lastS‘∅)
5655a1i 11 . . 3 (𝜑 → ∀𝑖 ∈ (0..^((♯‘∅) − 1))(∅‘𝑖) < (lastS‘∅))
57 simp-6r 788 . . . . . . . . . . . . 13 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → 𝑑 ∈ ( < Chain𝐴))
5857chnwrd 32981 . . . . . . . . . . . 12 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → 𝑑 ∈ Word 𝐴)
59 ccatws1len 14654 . . . . . . . . . . . 12 (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
6058, 59syl 17 . . . . . . . . . . 11 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
61 simpr 484 . . . . . . . . . . . . . 14 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → 𝑑 = ∅)
6261fveq2d 6910 . . . . . . . . . . . . 13 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → (♯‘𝑑) = (♯‘∅))
6362, 37eqtrdi 2790 . . . . . . . . . . . 12 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → (♯‘𝑑) = 0)
6463oveq1d 7445 . . . . . . . . . . 11 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → ((♯‘𝑑) + 1) = (0 + 1))
65 0p1e1 12385 . . . . . . . . . . . 12 (0 + 1) = 1
6665a1i 11 . . . . . . . . . . 11 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → (0 + 1) = 1)
6760, 64, 663eqtrd 2778 . . . . . . . . . 10 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = 1)
6867oveq1d 7445 . . . . . . . . 9 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → ((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1) = (1 − 1))
69 1m1e0 12335 . . . . . . . . 9 (1 − 1) = 0
7068, 69eqtrdi 2790 . . . . . . . 8 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → ((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1) = 0)
7170oveq2d 7446 . . . . . . 7 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1)) = (0..^0))
72 fzo0 13719 . . . . . . 7 (0..^0) = ∅
7371, 72eqtrdi 2790 . . . . . 6 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1)) = ∅)
74 simplr 769 . . . . . . 7 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1)))
7574ne0d 4347 . . . . . 6 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1)) ≠ ∅)
7673, 75pm2.21ddne 3023 . . . . 5 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 = ∅) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
77 chnub.1 . . . . . . . 8 (𝜑< Po 𝐴)
7877ad7antr 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𝐴))
8079chnwrd 32981 . . . . . . . . . . 11 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → 𝑑 ∈ Word 𝐴)
8180adantr 480 . . . . . . . . . 10 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → 𝑑 ∈ Word 𝐴)
82 simp-5r 786 . . . . . . . . . . 11 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → 𝑥𝐴)
8382adantr 480 . . . . . . . . . 10 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → 𝑥𝐴)
84 ccatws1cl 14650 . . . . . . . . . 10 ((𝑑 ∈ Word 𝐴𝑥𝐴) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
8581, 83, 84syl2anc 584 . . . . . . . . 9 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
86 lencl 14567 . . . . . . . . . . . . . . . 16 (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈ ℕ0)
8780, 86syl 17 . . . . . . . . . . . . . . 15 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ∈ ℕ0)
8887nn0zd 12636 . . . . . . . . . . . . . 14 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ∈ ℤ)
89 1zzd 12645 . . . . . . . . . . . . . 14 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → 1 ∈ ℤ)
9088, 89zsubcld 12724 . . . . . . . . . . . . 13 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘𝑑) − 1) ∈ ℤ)
9188peano2zd 12722 . . . . . . . . . . . . 13 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘𝑑) + 1) ∈ ℤ)
9290zred 12719 . . . . . . . . . . . . . 14 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘𝑑) − 1) ∈ ℝ)
9391zred 12719 . . . . . . . . . . . . . 14 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘𝑑) + 1) ∈ ℝ)
94 simpr 484 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → 𝑑 ≠ ∅)
95 hasheq0 14398 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) = 0 ↔ 𝑑 = ∅))
9695necon3bid 2982 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) ≠ 0 ↔ 𝑑 ≠ ∅))
9796biimpar 477 . . . . . . . . . . . . . . . . . 18 ((𝑑 ∈ Word 𝐴𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0)
9880, 94, 97syl2anc 584 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0)
99 elnnne0 12537 . . . . . . . . . . . . . . . . 17 ((♯‘𝑑) ∈ ℕ ↔ ((♯‘𝑑) ∈ ℕ0 ∧ (♯‘𝑑) ≠ 0))
10087, 98, 99sylanbrc 583 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ∈ ℕ)
101100nnred 12278 . . . . . . . . . . . . . . 15 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ∈ ℝ)
102101ltm1d 12197 . . . . . . . . . . . . . . 15 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘𝑑) − 1) < (♯‘𝑑))
103101ltp1d 12195 . . . . . . . . . . . . . . 15 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (♯‘𝑑) < ((♯‘𝑑) + 1))
10492, 101, 93, 102, 103lttrd 11419 . . . . . . . . . . . . . 14 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘𝑑) − 1) < ((♯‘𝑑) + 1))
10592, 93, 104ltled 11406 . . . . . . . . . . . . 13 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘𝑑) − 1) ≤ ((♯‘𝑑) + 1))
106 eluz2 12881 . . . . . . . . . . . . 13 (((♯‘𝑑) + 1) ∈ (ℤ‘((♯‘𝑑) − 1)) ↔ (((♯‘𝑑) − 1) ∈ ℤ ∧ ((♯‘𝑑) + 1) ∈ ℤ ∧ ((♯‘𝑑) − 1) ≤ ((♯‘𝑑) + 1)))
10790, 91, 105, 106syl3anbrc 1342 . . . . . . . . . . . 12 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘𝑑) + 1) ∈ (ℤ‘((♯‘𝑑) − 1)))
108 fzoss2 13723 . . . . . . . . . . . 12 (((♯‘𝑑) + 1) ∈ (ℤ‘((♯‘𝑑) − 1)) → (0..^((♯‘𝑑) − 1)) ⊆ (0..^((♯‘𝑑) + 1)))
109107, 108syl 17 . . . . . . . . . . 11 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (0..^((♯‘𝑑) − 1)) ⊆ (0..^((♯‘𝑑) + 1)))
110109sselda 3994 . . . . . . . . . 10 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → 𝑗 ∈ (0..^((♯‘𝑑) + 1)))
11181, 59syl 17 . . . . . . . . . . 11 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
112111oveq2d 7446 . . . . . . . . . 10 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩))) = (0..^((♯‘𝑑) + 1)))
113110, 112eleqtrrd 2841 . . . . . . . . 9 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩))))
114 wrdsymbcl 14561 . . . . . . . . 9 (((𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∈ 𝐴)
11585, 113, 114syl2anc 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 14602 . . . . . . . . 9 ((𝑑 ∈ Word 𝐴𝑑 ≠ ∅) → (lastS‘𝑑) ∈ 𝐴)
11881, 116, 117syl2anc 584 . . . . . . . 8 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (lastS‘𝑑) ∈ 𝐴)
119 lswccats1 14668 . . . . . . . . . . 11 ((𝑑 ∈ Word 𝐴𝑥𝐴) → (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) = 𝑥)
12080, 82, 119syl2anc 584 . . . . . . . . . 10 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) = 𝑥)
121120adantr 480 . . . . . . . . 9 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) = 𝑥)
122121, 83eqeltrd 2838 . . . . . . . 8 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) ∈ 𝐴)
123115, 118, 1223jca 1127 . . . . . . 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)))
12559oveq1d 7445 . . . . . . . . . . . . . 14 (𝑑 ∈ Word 𝐴 → ((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1) = (((♯‘𝑑) + 1) − 1))
12680, 125syl 17 . . . . . . . . . . . . 13 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1) = (((♯‘𝑑) + 1) − 1))
127100nncnd 12279 . . . . . . . . . . . . . 14 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ∈ ℂ)
128 1cnd 11253 . . . . . . . . . . . . . 14 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → 1 ∈ ℂ)
129127, 128pncand 11618 . . . . . . . . . . . . 13 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (((♯‘𝑑) + 1) − 1) = (♯‘𝑑))
130126, 129eqtrd 2774 . . . . . . . . . . . 12 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1) = (♯‘𝑑))
131130oveq2d 7446 . . . . . . . . . . 11 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1)) = (0..^(♯‘𝑑)))
132124, 131eleqtrd 2840 . . . . . . . . . 10 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → 𝑗 ∈ (0..^(♯‘𝑑)))
133132adantr 480 . . . . . . . . 9 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → 𝑗 ∈ (0..^(♯‘𝑑)))
134 ccats1val1 14660 . . . . . . . . 9 ((𝑑 ∈ Word 𝐴𝑗 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑𝑗))
13581, 133, 134syl2anc 584 . . . . . . . 8 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑𝑗))
136 fveq2 6906 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝑑𝑖) = (𝑑𝑗))
137136breq1d 5157 . . . . . . . . 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)))
140137, 138, 139rspcdva 3622 . . . . . . . 8 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (𝑑𝑗) < (lastS‘𝑑))
141135, 140eqbrtrd 5169 . . . . . . 7 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘𝑑))
142 simp-4r 784 . . . . . . . . . 10 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥))
14394neneqd 2942 . . . . . . . . . 10 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ¬ 𝑑 = ∅)
144142, 143orcnd 878 . . . . . . . . 9 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (lastS‘𝑑) < 𝑥)
145144adantr 480 . . . . . . . 8 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (lastS‘𝑑) < 𝑥)
146145, 121breqtrrd 5175 . . . . . . 7 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → (lastS‘𝑑) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
147 potr 5609 . . . . . . . 8 (( < Po 𝐴 ∧ (((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∈ 𝐴 ∧ (lastS‘𝑑) ∈ 𝐴 ∧ (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) ∈ 𝐴)) → ((((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘𝑑) ∧ (lastS‘𝑑) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩))))
148147imp 406 . . . . . . 7 ((( < Po 𝐴 ∧ (((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∈ 𝐴 ∧ (lastS‘𝑑) ∈ 𝐴 ∧ (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) ∈ 𝐴)) ∧ (((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘𝑑) ∧ (lastS‘𝑑) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
14978, 123, 141, 146, 148syl22anc 839 . . . . . 6 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ∈ (0..^((♯‘𝑑) − 1))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
150144adantr 480 . . . . . . 7 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → (lastS‘𝑑) < 𝑥)
15180adantr 480 . . . . . . . . 9 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → 𝑑 ∈ Word 𝐴)
152 simp-6r 788 . . . . . . . . . 10 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → 𝑥𝐴)
153152s1cld 14637 . . . . . . . . 9 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
154100adantr 480 . . . . . . . . . 10 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → (♯‘𝑑) ∈ ℕ)
155 fzo0end 13793 . . . . . . . . . 10 ((♯‘𝑑) ∈ ℕ → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
156154, 155syl 17 . . . . . . . . 9 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
157 ccatval1 14611 . . . . . . . . 9 ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
158151, 153, 156, 157syl3anc 1370 . . . . . . . 8 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
159 simpr 484 . . . . . . . . 9 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → 𝑗 = ((♯‘𝑑) − 1))
160159fveq2d 6910 . . . . . . . 8 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)))
161 lsw 14598 . . . . . . . . 9 (𝑑 ∈ Word 𝐴 → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
162151, 161syl 17 . . . . . . . 8 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
163158, 160, 1623eqtr4d 2784 . . . . . . 7 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (lastS‘𝑑))
164120adantr 480 . . . . . . 7 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) = 𝑥)
165150, 163, 1643brtr4d 5179 . . . . . 6 ((((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = ((♯‘𝑑) − 1)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
16665fveq2i 6909 . . . . . . . . . . 11 (ℤ‘(0 + 1)) = (ℤ‘1)
167 nnuz 12918 . . . . . . . . . . 11 ℕ = (ℤ‘1)
168166, 167eqtr4i 2765 . . . . . . . . . 10 (ℤ‘(0 + 1)) = ℕ
169100, 168eleqtrrdi 2849 . . . . . . . . 9 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ∈ (ℤ‘(0 + 1)))
170 fzosplitsnm1 13775 . . . . . . . . 9 ((0 ∈ ℤ ∧ (♯‘𝑑) ∈ (ℤ‘(0 + 1))) → (0..^(♯‘𝑑)) = ((0..^((♯‘𝑑) − 1)) ∪ {((♯‘𝑑) − 1)}))
17146, 169, 170sylancr 587 . . . . . . . 8 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (0..^(♯‘𝑑)) = ((0..^((♯‘𝑑) − 1)) ∪ {((♯‘𝑑) − 1)}))
172132, 171eleqtrd 2840 . . . . . . 7 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → 𝑗 ∈ ((0..^((♯‘𝑑) − 1)) ∪ {((♯‘𝑑) − 1)}))
173 elunsn 4687 . . . . . . . 8 (𝑗 ∈ ((0..^((♯‘𝑑) − 1)) ∪ {((♯‘𝑑) − 1)}) → (𝑗 ∈ ((0..^((♯‘𝑑) − 1)) ∪ {((♯‘𝑑) − 1)}) ↔ (𝑗 ∈ (0..^((♯‘𝑑) − 1)) ∨ 𝑗 = ((♯‘𝑑) − 1))))
174173ibi 267 . . . . . . 7 (𝑗 ∈ ((0..^((♯‘𝑑) − 1)) ∪ {((♯‘𝑑) − 1)}) → (𝑗 ∈ (0..^((♯‘𝑑) − 1)) ∨ 𝑗 = ((♯‘𝑑) − 1)))
175172, 174syl 17 . . . . . 6 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → (𝑗 ∈ (0..^((♯‘𝑑) − 1)) ∨ 𝑗 = ((♯‘𝑑) − 1)))
176149, 165, 175mpjaodan 960 . . . . 5 (((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) ∧ 𝑑 ≠ ∅) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
17776, 176pm2.61dane 3026 . . . 4 ((((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
178177ralrimiva 3143 . . 3 (((((𝜑𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ ∀𝑖 ∈ (0..^((♯‘𝑑) − 1))(𝑑𝑖) < (lastS‘𝑑)) → ∀𝑗 ∈ (0..^((♯‘(𝑑 ++ ⟨“𝑥”⟩)) − 1))((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) < (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
1799, 16, 27, 34, 35, 56, 178chnind 32984 . 2 (𝜑 → ∀𝑖 ∈ (0..^((♯‘𝐶) − 1))(𝐶𝑖) < (lastS‘𝐶))
180 chnub.3 . 2 (𝜑𝐼 ∈ (0..^((♯‘𝐶) − 1)))
1812, 179, 180rspcdva 3622 1 (𝜑 → (𝐶𝐼) < (lastS‘𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  cun 3960  wss 3962  c0 4338  {csn 4630   class class class wbr 5147   Po wpo 5594  cfv 6562  (class class class)co 7430  0cc0 11152  1c1 11153   + caddc 11155  cle 11293  cmin 11489  -cneg 11490  cn 12263  0cn0 12523  cz 12610  cuz 12875  ..^cfzo 13690  chash 14365  Word cword 14548  lastSclsw 14596   ++ cconcat 14604  ⟨“cs1 14629  Chaincchn 32978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-hash 14366  df-word 14549  df-lsw 14597  df-concat 14605  df-s1 14630  df-substr 14675  df-pfx 14705  df-chn 32979
This theorem is referenced by:  chnlt  32986
  Copyright terms: Public domain W3C validator