chnind - Mathbox for Thierry Arnoux

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

Theorem chnind 32883

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

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

**Assertion**
Ref	Expression
chnind	⊢ (𝜑 → 𝜂)

Distinct variable groups: < ,𝑐,𝑑,𝑥 𝐴,𝑐,𝑑,𝑥 𝐶,𝑐 𝜑,𝑐,𝑑,𝑥 𝜂,𝑐 𝜃,𝑐 𝜏,𝑐 𝜓,𝑑,𝑥 Allowed substitution hints: 𝜓(𝑐) 𝜒(𝑥,𝑐,𝑑) 𝜃(𝑥,𝑑) 𝜏(𝑥,𝑑) 𝜂(𝑥,𝑑) 𝐶(𝑥,𝑑)

Proof of Theorem chnind Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		chnind.6	. . 3 ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))
2	1	chnwrd 32880	. 2 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
3		id 22	. 2 ⊢ (𝜑 → 𝜑)
4		ischn 32879	. . . 4 ⊢ (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
5	1, 4	sylib 217	. . 3 ⊢ (𝜑 → (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
6	5	simprd 494	. 2 ⊢ (𝜑 → ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))
7		dmeq 5902	. . . . . . . 8 ⊢ (𝑐 = ∅ → dom 𝑐 = dom ∅)
8	7	difeq1d 4117	. . . . . . 7 ⊢ (𝑐 = ∅ → (dom 𝑐 ∖ {0}) = (dom ∅ ∖ {0}))
9		fveq1 6892	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘(𝑖 − 1)) = (∅‘(𝑖 − 1)))
10		fveq1 6892	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘𝑖) = (∅‘𝑖))
11	9, 10	breq12d 5158	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (∅‘(𝑖 − 1)) < (∅‘𝑖)))
12	8, 11	raleqbidv 3330	. . . . . 6 ⊢ (𝑐 = ∅ → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)))
13	12	anbi2d 628	. . . . 5 ⊢ (𝑐 = ∅ → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖))))
14		chnind.1	. . . . 5 ⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))
15	13, 14	imbi12d 343	. . . 4 ⊢ (𝑐 = ∅ → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)))
16		dmeq 5902	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → dom 𝑐 = dom 𝑑)
17	16	difeq1d 4117	. . . . . . 7 ⊢ (𝑐 = 𝑑 → (dom 𝑐 ∖ {0}) = (dom 𝑑 ∖ {0}))
18		fveq1 6892	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘(𝑖 − 1)) = (𝑑‘(𝑖 − 1)))
19		fveq1 6892	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑖) = (𝑑‘𝑖))
20	18, 19	breq12d 5158	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
21	17, 20	raleqbidv 3330	. . . . . 6 ⊢ (𝑐 = 𝑑 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
22	21	anbi2d 628	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))))
23		chnind.2	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))
24	22, 23	imbi12d 343	. . . 4 ⊢ (𝑐 = 𝑑 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃)))
25		dmeq 5902	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → dom 𝑐 = dom (𝑑 ++ ⟨“𝑥”⟩))
26	25	difeq1d 4117	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (dom 𝑐 ∖ {0}) = (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
27		fveq1 6892	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)))
28		fveq1 6892	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))
29	27, 28	breq12d 5158	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
30	26, 29	raleqbidv 3330	. . . . . 6 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
31	30	anbi2d 628	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))))
32		chnind.3	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))
33	31, 32	imbi12d 343	. . . 4 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
34		dmeq 5902	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → dom 𝑐 = dom 𝐶)
35	34	difeq1d 4117	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (dom 𝑐 ∖ {0}) = (dom 𝐶 ∖ {0}))
36		fveq1 6892	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘(𝑖 − 1)) = (𝐶‘(𝑖 − 1)))
37		fveq1 6892	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑖) = (𝐶‘𝑖))
38	36, 37	breq12d 5158	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
39	35, 38	raleqbidv 3330	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
40	39	anbi2d 628	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))))
41		chnind.4	. . . . 5 ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))
42	40, 41	imbi12d 343	. . . 4 ⊢ (𝑐 = 𝐶 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂)))
43		chnind.7	. . . . 5 ⊢ (𝜑 → 𝜒)
44	43	adantr 479	. . . 4 ⊢ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)
45		simpllr 774	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜑)
46		simp-4l 781	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
47		simpll 765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑑 ∈ Word 𝐴)
48		simplr 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑥 ∈ 𝐴)
49	48	s1cld 14606	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → ⟨“𝑥”⟩ ∈ Word 𝐴)
50	47, 49	ccatdmss 32816	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → dom 𝑑 ⊆ dom (𝑑 ++ ⟨“𝑥”⟩))
51	50	ssdifd 4137	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → (dom 𝑑 ∖ {0}) ⊆ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
52	51	sselda 3978	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → 𝑗 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
53		fvoveq1 7439	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)))
54		fveq2 6893	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
55	53, 54	breq12d 5158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
56	55	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ 𝑖 = 𝑗) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
57	52, 56	rspcdv 3599	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
58	57	imp 405	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
59		simp-4l 781	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
60	49	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
61		lencl 14536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈ ℕ₀)
62	59, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
63	62	nn0zd 12630	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℤ)
64		fzossrbm1 13709	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℤ → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
65	63, 64	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
66		fzossz 13700	. . . . . . . . . . . . . . . . . . 19 ⊢ (0..^(♯‘𝑑)) ⊆ ℤ
67		simplr 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (dom 𝑑 ∖ {0}))
68	67	eldifad 3958	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ dom 𝑑)
69		eqidd 2727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
70	69, 59	wrdfd 32800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑:(0..^(♯‘𝑑))⟶𝐴)
71	70	fdmd 6730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → dom 𝑑 = (0..^(♯‘𝑑)))
72	68, 71	eleqtrd 2828	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (0..^(♯‘𝑑)))
73	66, 72	sselid 3976	. . . . . . . . . . . . . . . . . 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 13731	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 ∈ (0..^(♯‘𝑑)) ∧ 𝑗 ≠ 0))
77	72, 75, 76	sylanbrc 581	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (1..^(♯‘𝑑)))
78		elfzom1b 13780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) → (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1))))
79	78	biimpa 475	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) ∧ 𝑗 ∈ (1..^(♯‘𝑑))) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
80	73, 63, 77, 79	syl21anc 836	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
81	65, 80	sseldd 3979	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^(♯‘𝑑)))
82		ccatval1 14580	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ (𝑗 − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
83	59, 60, 81, 82	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
84		ccatval1 14580	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ 𝑗 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
85	59, 60, 72, 84	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
86	58, 83, 85	3brtr3d 5176	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
87	86	an32s 650	. . . . . . . . . . . . 13 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
88	87	adantllr 717	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
89	88	ralrimiva 3136	. . . . . . . . . . 11 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
90	89	an32s 650	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
91		ischn 32879	. . . . . . . . . 10 ⊢ (𝑑 ∈ ( < Chain𝐴) ↔ (𝑑 ∈ Word 𝐴 ∧ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
92	46, 90, 91	sylanbrc 581	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ ( < Chain𝐴))
93	45, 92	jca 510	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)))
94		simp-4r 782	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑥 ∈ 𝐴)
95		lsw 14567	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ Word 𝐴 → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
96	95	ad5antr 732	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
97		simp-4l 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
98		fzonn0p1 13757	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℕ₀ → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
99	97, 61, 98	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
100		ccatws1len 14623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
101	100	ad4antr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
102	101	eqcomd 2732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ((♯‘𝑑) + 1) = (♯‘(𝑑 ++ ⟨“𝑥”⟩)))
103		ccatws1cl 14619	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
104	103	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
105	102, 104	wrdfd 32800	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩):(0..^((♯‘𝑑) + 1))⟶𝐴)
106	105	fdmd 6730	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → dom (𝑑 ++ ⟨“𝑥”⟩) = (0..^((♯‘𝑑) + 1)))
107	99, 106	eleqtrrd 2829	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ dom (𝑑 ++ ⟨“𝑥”⟩))
108		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ¬ 𝑑 = ∅)
109	108	neqned 2937	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ≠ ∅)
110		hasheq0 14375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) = 0 ↔ 𝑑 = ∅))
111	110	necon3bid 2975	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) ≠ 0 ↔ 𝑑 ≠ ∅))
112	111	biimpar 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0)
113	97, 109, 112	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ≠ 0)
114	107, 113	eldifsnd 4786	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
115		fvoveq1 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)))
116		fveq2 6893	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
117	115, 116	breq12d 5158	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (♯‘𝑑) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
118	117	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ 𝑖 = (♯‘𝑑)) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
119	114, 118	rspcdv 3599	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
120	119	imp 405	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
121	47	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
122	49	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
123	121, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
124	113	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ≠ 0)
125		elnnne0 12532	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑑) ∈ ℕ ↔ ((♯‘𝑑) ∈ ℕ₀ ∧ (♯‘𝑑) ≠ 0))
126	123, 124, 125	sylanbrc 581	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ)
127		fzo0end 13772	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑑) ∈ ℕ → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
128	126, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
129		ccatval1 14580	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
130	121, 122, 128, 129	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
131	48	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑥 ∈ 𝐴)
132		eqidd 2727	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
133		ccats1val2 14630	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ (♯‘𝑑) = (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
134	121, 131, 132, 133	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
135	120, 130, 134	3brtr3d 5176	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘((♯‘𝑑) − 1)) < 𝑥)
136	96, 135	eqbrtrd 5167	. . . . . . . . . . 11 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) < 𝑥)
137	136	an42ds 32377	. . . . . . . . . 10 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) ∧ ¬ 𝑑 = ∅) → (lastS‘𝑑) < 𝑥)
138	137	ex 411	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (¬ 𝑑 = ∅ → (lastS‘𝑑) < 𝑥))
139	138	orrd 861	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥))
140		simpr 483	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜃)
141		chnind.8	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)
142	93, 94, 139, 140, 141	syl1111anc 838	. . . . . . 7 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜏)
143	142	ex 411	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏))
144	143	expl 456	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏)))
145	87	ralrimiva 3136	. . . . . . 7 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
146		fvoveq1 7439	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘(𝑖 − 1)) = (𝑑‘(𝑗 − 1)))
147		fveq2 6893	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘𝑖) = (𝑑‘𝑗))
148	146, 147	breq12d 5158	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → ((𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
149	148	cbvralvw 3225	. . . . . . 7 ⊢ (∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
150	145, 149	sylibr 233	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))
151	150	expl 456	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
152	144, 151	a2and 843	. . . 4 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
153	15, 24, 33, 42, 44, 152	wrdind 14725	. . 3 ⊢ (𝐶 ∈ Word 𝐴 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂))
154	153	imp 405	. 2 ⊢ ((𝐶 ∈ Word 𝐴 ∧ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) → 𝜂)
155	2, 3, 6, 154	syl12anc 835	1 ⊢ (𝜑 → 𝜂)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 845 = wceq 1534 ∈ wcel 2099 ≠ wne 2930 ∀wral 3051 ∖ cdif 3943 ⊆ wss 3946 ∅c0 4322 {csn 4623 class class class wbr 5145 dom cdm 5674 ‘cfv 6546 (class class class)co 7416 0cc0 11149 1c1 11150 + caddc 11152 − cmin 11485 ℕcn 12258 ℕ₀cn0 12518 ℤcz 12604 ..^cfzo 13675 ♯chash 14342 Word cword 14517 lastSclsw 14565 ++ cconcat 14573 ⟨“cs1 14598 Chaincchn 32877

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5282 ax-sep 5296 ax-nul 5303 ax-pow 5361 ax-pr 5425 ax-un 7738 ax-cnex 11205 ax-resscn 11206 ax-1cn 11207 ax-icn 11208 ax-addcl 11209 ax-addrcl 11210 ax-mulcl 11211 ax-mulrcl 11212 ax-mulcom 11213 ax-addass 11214 ax-mulass 11215 ax-distr 11216 ax-i2m1 11217 ax-1ne0 11218 ax-1rid 11219 ax-rnegex 11220 ax-rrecex 11221 ax-cnre 11222 ax-pre-lttri 11223 ax-pre-lttrn 11224 ax-pre-ltadd 11225 ax-pre-mulgt0 11226

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3966 df-nul 4323 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4906 df-int 4947 df-iun 4995 df-br 5146 df-opab 5208 df-mpt 5229 df-tr 5263 df-id 5572 df-eprel 5578 df-po 5586 df-so 5587 df-fr 5629 df-we 5631 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-pred 6304 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6498 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-riota 7372 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7869 df-1st 7995 df-2nd 7996 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-er 8726 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-card 9975 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11487 df-neg 11488 df-nn 12259 df-n0 12519 df-xnn0 12591 df-z 12605 df-uz 12869 df-fz 13533 df-fzo 13676 df-hash 14343 df-word 14518 df-lsw 14566 df-concat 14574 df-s1 14599 df-substr 14644 df-pfx 14674 df-chn 32878

This theorem is referenced by: chnub 32884 fldext2chn 33601

W3C validator