chnind - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > chnind		Structured version Visualization version GIF version

Theorem chnind 18636

Description: Induction over a chain. See nnind 12225 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 18623	. 2 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
3		id 22	. 2 ⊢ (𝜑 → 𝜑)
4		ischn 18622	. . . 4 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
5	1, 4	sylib 220	. . 3 ⊢ (𝜑 → (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
6	5	simprd 499	. 2 ⊢ (𝜑 → ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))
7		dmeq 5877	. . . . . . . 8 ⊢ (𝑐 = ∅ → dom 𝑐 = dom ∅)
8	7	difeq1d 4079	. . . . . . 7 ⊢ (𝑐 = ∅ → (dom 𝑐 ∖ {0}) = (dom ∅ ∖ {0}))
9		fveq1 6862	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘(𝑖 − 1)) = (∅‘(𝑖 − 1)))
10		fveq1 6862	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘𝑖) = (∅‘𝑖))
11	9, 10	breq12d 5112	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (∅‘(𝑖 − 1)) < (∅‘𝑖)))
12	8, 11	raleqbidv 3335	. . . . . 6 ⊢ (𝑐 = ∅ → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)))
13	12	anbi2d 639	. . . . 5 ⊢ (𝑐 = ∅ → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖))))
14		chnind.1	. . . . 5 ⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))
15	13, 14	imbi12d 346	. . . 4 ⊢ (𝑐 = ∅ → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)))
16		dmeq 5877	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → dom 𝑐 = dom 𝑑)
17	16	difeq1d 4079	. . . . . . 7 ⊢ (𝑐 = 𝑑 → (dom 𝑐 ∖ {0}) = (dom 𝑑 ∖ {0}))
18		fveq1 6862	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘(𝑖 − 1)) = (𝑑‘(𝑖 − 1)))
19		fveq1 6862	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑖) = (𝑑‘𝑖))
20	18, 19	breq12d 5112	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
21	17, 20	raleqbidv 3335	. . . . . 6 ⊢ (𝑐 = 𝑑 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
22	21	anbi2d 639	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))))
23		chnind.2	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))
24	22, 23	imbi12d 346	. . . 4 ⊢ (𝑐 = 𝑑 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃)))
25		dmeq 5877	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → dom 𝑐 = dom (𝑑 ++ ⟨“𝑥”⟩))
26	25	difeq1d 4079	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (dom 𝑐 ∖ {0}) = (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
27		fveq1 6862	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)))
28		fveq1 6862	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))
29	27, 28	breq12d 5112	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
30	26, 29	raleqbidv 3335	. . . . . 6 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
31	30	anbi2d 639	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))))
32		chnind.3	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))
33	31, 32	imbi12d 346	. . . 4 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
34		dmeq 5877	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → dom 𝑐 = dom 𝐶)
35	34	difeq1d 4079	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (dom 𝑐 ∖ {0}) = (dom 𝐶 ∖ {0}))
36		fveq1 6862	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘(𝑖 − 1)) = (𝐶‘(𝑖 − 1)))
37		fveq1 6862	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑖) = (𝐶‘𝑖))
38	36, 37	breq12d 5112	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
39	35, 38	raleqbidv 3335	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
40	39	anbi2d 639	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))))
41		chnind.4	. . . . 5 ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))
42	40, 41	imbi12d 346	. . . 4 ⊢ (𝑐 = 𝐶 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂)))
43		chnind.7	. . . . 5 ⊢ (𝜑 → 𝜒)
44	43	adantr 484	. . . 4 ⊢ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)
45		simpllr 785	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜑)
46		simp-4l 792	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
47		simpll 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑑 ∈ Word 𝐴)
48		simplr 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑥 ∈ 𝐴)
49	48	s1cld 14614	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → ⟨“𝑥”⟩ ∈ Word 𝐴)
50	47, 49	ccatdmss 14592	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → dom 𝑑 ⊆ dom (𝑑 ++ ⟨“𝑥”⟩))
51	50	ssdifd 4098	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → (dom 𝑑 ∖ {0}) ⊆ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
52	51	sselda 3936	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → 𝑗 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
53		fvoveq1 7415	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)))
54		fveq2 6863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
55	53, 54	breq12d 5112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
56	55	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ 𝑖 = 𝑗) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
57	52, 56	rspcdv 3573	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
58	57	imp 410	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
59		simp-4l 792	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
60	49	ad2antrr 736	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
61		lencl 14543	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈ ℕ₀)
62	59, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
63	62	nn0zd 12590	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℤ)
64		fzossrbm1 13691	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℤ → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
65	63, 64	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
66		fzossz 13682	. . . . . . . . . . . . . . . . . . 19 ⊢ (0..^(♯‘𝑑)) ⊆ ℤ
67		simplr 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (dom 𝑑 ∖ {0}))
68	67	eldifad 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ dom 𝑑)
69		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
70	69, 59	wrdfd 14529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑:(0..^(♯‘𝑑))⟶𝐴)
71	70	fdmd 6698	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → dom 𝑑 = (0..^(♯‘𝑑)))
72	68, 71	eleqtrd 2863	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (0..^(♯‘𝑑)))
73	66, 72	sselid 3934	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ ℤ)
74		eldifsni 4749	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (dom 𝑑 ∖ {0}) → 𝑗 ≠ 0)
75	67, 74	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ≠ 0)
76		fzo1fzo0n0 13718	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 ∈ (0..^(♯‘𝑑)) ∧ 𝑗 ≠ 0))
77	72, 75, 76	sylanbrc 592	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (1..^(♯‘𝑑)))
78		elfzom1b 13769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) → (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1))))
79	78	biimpa 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) ∧ 𝑗 ∈ (1..^(♯‘𝑑))) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
80	73, 63, 77, 79	syl21anc 848	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
81	65, 80	sseldd 3937	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^(♯‘𝑑)))
82		ccatval1 14587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ (𝑗 − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
83	59, 60, 81, 82	syl3anc 1389	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
84		ccatval1 14587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ 𝑗 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
85	59, 60, 72, 84	syl3anc 1389	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
86	58, 83, 85	3brtr3d 5130	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
87	86	an32s 662	. . . . . . . . . . . . 13 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
88	87	adantllr 729	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
89	88	ralrimiva 3153	. . . . . . . . . . 11 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
90	89	an32s 662	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
91		ischn 18622	. . . . . . . . . 10 ⊢ (𝑑 ∈ ( < Chain 𝐴) ↔ (𝑑 ∈ Word 𝐴 ∧ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
92	46, 90, 91	sylanbrc 592	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ ( < Chain 𝐴))
93	45, 92	jca 519	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)))
94		simp-4r 793	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑥 ∈ 𝐴)
95		lsw 14574	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ Word 𝐴 → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
96	95	ad5antr 744	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
97		simp-4l 792	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
98		fzonn0p1 13745	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℕ₀ → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
99	97, 61, 98	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
100		ccatws1len 14631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
101	100	ad4antr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
102	101	eqcomd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ((♯‘𝑑) + 1) = (♯‘(𝑑 ++ ⟨“𝑥”⟩)))
103		ccatws1cl 14627	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
104	103	ad3antrrr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
105	102, 104	wrdfd 14529	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩):(0..^((♯‘𝑑) + 1))⟶𝐴)
106	105	fdmd 6698	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → dom (𝑑 ++ ⟨“𝑥”⟩) = (0..^((♯‘𝑑) + 1)))
107	99, 106	eleqtrrd 2864	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ dom (𝑑 ++ ⟨“𝑥”⟩))
108		simplr 778	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ¬ 𝑑 = ∅)
109	108	neqned 2963	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ≠ ∅)
110		hasheq0 14373	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) = 0 ↔ 𝑑 = ∅))
111	110	necon3bid 3000	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) ≠ 0 ↔ 𝑑 ≠ ∅))
112	111	biimpar 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0)
113	97, 109, 112	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ≠ 0)
114	107, 113	eldifsnd 4746	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
115		fvoveq1 7415	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)))
116		fveq2 6863	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
117	115, 116	breq12d 5112	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (♯‘𝑑) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
118	117	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ 𝑖 = (♯‘𝑑)) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
119	114, 118	rspcdv 3573	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
120	119	imp 410	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
121	47	ad3antrrr 740	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
122	49	ad3antrrr 740	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
123	121, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
124	113	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ≠ 0)
125		elnnne0 12492	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑑) ∈ ℕ ↔ ((♯‘𝑑) ∈ ℕ₀ ∧ (♯‘𝑑) ≠ 0))
126	123, 124, 125	sylanbrc 592	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ)
127		fzo0end 13761	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑑) ∈ ℕ → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
128	126, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
129		ccatval1 14587	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
130	121, 122, 128, 129	syl3anc 1389	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
131	48	ad3antrrr 740	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑥 ∈ 𝐴)
132		eqidd 2762	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
133		ccats1val2 14638	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ (♯‘𝑑) = (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
134	121, 131, 132, 133	syl3anc 1389	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
135	120, 130, 134	3brtr3d 5130	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘((♯‘𝑑) − 1)) < 𝑥)
136	96, 135	eqbrtrd 5121	. . . . . . . . . . 11 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) < 𝑥)
137	136	an42ds 1509	. . . . . . . . . 10 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) ∧ ¬ 𝑑 = ∅) → (lastS‘𝑑) < 𝑥)
138	137	ex 416	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (¬ 𝑑 = ∅ → (lastS‘𝑑) < 𝑥))
139	138	orrd 874	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥))
140		simpr 488	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜃)
141		chnind.8	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)
142	93, 94, 139, 140, 141	syl1111anc 851	. . . . . . 7 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜏)
143	142	ex 416	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏))
144	143	expl 461	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏)))
145	87	ralrimiva 3153	. . . . . . 7 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
146		fvoveq1 7415	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘(𝑖 − 1)) = (𝑑‘(𝑗 − 1)))
147		fveq2 6863	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘𝑖) = (𝑑‘𝑗))
148	146, 147	breq12d 5112	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → ((𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
149	148	cbvralvw 3239	. . . . . . 7 ⊢ (∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
150	145, 149	sylibr 236	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))
151	150	expl 461	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
152	144, 151	a2and 856	. . . 4 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
153	15, 24, 33, 42, 44, 152	wrdind 14732	. . 3 ⊢ (𝐶 ∈ Word 𝐴 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂))
154	153	imp 410	. 2 ⊢ ((𝐶 ∈ Word 𝐴 ∧ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) → 𝜂)
155	2, 3, 6, 154	syl12anc 847	1 ⊢ (𝜑 → 𝜂)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 ∖ cdif 3901 ⊆ wss 3904 ∅c0 4285 {csn 4581 class class class wbr 5099 dom cdm 5645 ‘cfv 6517 (class class class)co 7392 0cc0 11070 1c1 11071 + caddc 11073 − cmin 11411 ℕcn 12207 ℕ₀cn0 12478 ℤcz 12565 ..^cfzo 13656 ♯chash 14340 Word cword 14523 lastSclsw 14572 ++ cconcat 14580 ⟨“cs1 14606 Chain cchn 18620

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-om 7843 df-1st 7966 df-2nd 7967 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-er 8673 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-card 9894 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-nn 12208 df-n0 12479 df-xnn0 12552 df-z 12566 df-uz 12837 df-fz 13510 df-fzo 13657 df-hash 14341 df-word 14524 df-lsw 14573 df-concat 14581 df-s1 14607 df-substr 14652 df-pfx 14682 df-chn 18621

This theorem is referenced by: chnub 18637 fldext2chn 33986 chnerlem1 47422

W3C validator