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 18824

Description: Induction over a chain. See nnind 12380 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 18811	. 2 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
3		id 23	. 2 ⊢ (𝜑 → 𝜑)
4		ischn 18810	. . . 4 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
5	1, 4	sylib 221	. . 3 ⊢ (𝜑 → (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
6	5	simprd 501	. 2 ⊢ (𝜑 → ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))
7		dmeq 5892	. . . . . . . 8 ⊢ (𝑐 = ∅ → dom 𝑐 = dom ∅)
8	7	difeq1d 4065	. . . . . . 7 ⊢ (𝑐 = ∅ → (dom 𝑐 ∖ {0}) = (dom ∅ ∖ {0}))
9		fveq1 6907	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘(𝑖 − 1)) = (∅‘(𝑖 − 1)))
10		fveq1 6907	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘𝑖) = (∅‘𝑖))
11	9, 10	breq12d 5119	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (∅‘(𝑖 − 1)) < (∅‘𝑖)))
12	8, 11	raleqbidv 3338	. . . . . 6 ⊢ (𝑐 = ∅ → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)))
13	12	anbi2d 642	. . . . 5 ⊢ (𝑐 = ∅ → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖))))
14		chnind.1	. . . . 5 ⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))
15	13, 14	imbi12d 347	. . . 4 ⊢ (𝑐 = ∅ → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)))
16		dmeq 5892	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → dom 𝑐 = dom 𝑑)
17	16	difeq1d 4065	. . . . . . 7 ⊢ (𝑐 = 𝑑 → (dom 𝑐 ∖ {0}) = (dom 𝑑 ∖ {0}))
18		fveq1 6907	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘(𝑖 − 1)) = (𝑑‘(𝑖 − 1)))
19		fveq1 6907	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑖) = (𝑑‘𝑖))
20	18, 19	breq12d 5119	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
21	17, 20	raleqbidv 3338	. . . . . 6 ⊢ (𝑐 = 𝑑 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
22	21	anbi2d 642	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))))
23		chnind.2	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))
24	22, 23	imbi12d 347	. . . 4 ⊢ (𝑐 = 𝑑 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃)))
25		dmeq 5892	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → dom 𝑐 = dom (𝑑 ++ ⟨“𝑥”⟩))
26	25	difeq1d 4065	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (dom 𝑐 ∖ {0}) = (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
27		fveq1 6907	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)))
28		fveq1 6907	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))
29	27, 28	breq12d 5119	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
30	26, 29	raleqbidv 3338	. . . . . 6 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
31	30	anbi2d 642	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))))
32		chnind.3	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))
33	31, 32	imbi12d 347	. . . 4 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
34		dmeq 5892	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → dom 𝑐 = dom 𝐶)
35	34	difeq1d 4065	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (dom 𝑐 ∖ {0}) = (dom 𝐶 ∖ {0}))
36		fveq1 6907	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘(𝑖 − 1)) = (𝐶‘(𝑖 − 1)))
37		fveq1 6907	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑖) = (𝐶‘𝑖))
38	36, 37	breq12d 5119	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
39	35, 38	raleqbidv 3338	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
40	39	anbi2d 642	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))))
41		chnind.4	. . . . 5 ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))
42	40, 41	imbi12d 347	. . . 4 ⊢ (𝑐 = 𝐶 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂)))
43		chnind.7	. . . . 5 ⊢ (𝜑 → 𝜒)
44	43	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)
45		simpllr 788	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜑)
46		simp-4l 795	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
47		simpll 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑑 ∈ Word 𝐴)
48		simplr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑥 ∈ 𝐴)
49	48	s1cld 14777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → ⟨“𝑥”⟩ ∈ Word 𝐴)
50	47, 49	ccatdmss 14754	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → dom 𝑑 ⊆ dom (𝑑 ++ ⟨“𝑥”⟩))
51	50	ssdifd 4084	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → (dom 𝑑 ∖ {0}) ⊆ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
52	51	sselda 3913	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → 𝑗 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
53		fvoveq1 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)))
54		fveq2 6908	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
55	53, 54	breq12d 5119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
56	55	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ 𝑖 = 𝑗) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
57	52, 56	rspcdv 3572	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
58	57	imp 412	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
59		simp-4l 795	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
60	49	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
61		lencl 14705	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈ ℕ₀)
62	59, 61	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
63	62	nn0zd 12745	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℤ)
64		fzossrbm1 13850	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℤ → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
65	63, 64	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
66		fzossz 13841	. . . . . . . . . . . . . . . . . . 19 ⊢ (0..^(♯‘𝑑)) ⊆ ℤ
67		simplr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (dom 𝑑 ∖ {0}))
68	67	eldifad 4054	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ dom 𝑑)
69		eqidd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
70	69, 59	wrdfd 14691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑:(0..^(♯‘𝑑))⟶𝐴)
71	70	fdmd 6742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → dom 𝑑 = (0..^(♯‘𝑑)))
72	68, 71	eleqtrd 2866	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (0..^(♯‘𝑑)))
73	66, 72	sselid 3911	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ ℤ)
74		eldifsni 4753	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (dom 𝑑 ∖ {0}) → 𝑗 ≠ 0)
75	67, 74	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ≠ 0)
76		fzo1fzo0n0 13877	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 ∈ (0..^(♯‘𝑑)) ∧ 𝑗 ≠ 0))
77	72, 75, 76	sylanbrc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (1..^(♯‘𝑑)))
78		elfzom1b 13928	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) → (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1))))
79	78	biimpa 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) ∧ 𝑗 ∈ (1..^(♯‘𝑑))) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
80	73, 63, 77, 79	syl21anc 851	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
81	65, 80	sseldd 3914	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^(♯‘𝑑)))
82		ccatval1 14749	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ (𝑗 − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
83	59, 60, 81, 82	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
84		ccatval1 14749	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ 𝑗 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
85	59, 60, 72, 84	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
86	58, 83, 85	3brtr3d 5139	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
87	86	an32s 665	. . . . . . . . . . . . 13 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
88	87	adantllr 732	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
89	88	ralrimiva 3158	. . . . . . . . . . 11 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
90	89	an32s 665	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
91		ischn 18810	. . . . . . . . . 10 ⊢ (𝑑 ∈ ( < Chain 𝐴) ↔ (𝑑 ∈ Word 𝐴 ∧ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
92	46, 90, 91	sylanbrc 595	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ ( < Chain 𝐴))
93	45, 92	jca 521	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)))
94		simp-4r 796	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑥 ∈ 𝐴)
95		lsw 14736	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ Word 𝐴 → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
96	95	ad5antr 747	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
97		simp-4l 795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
98		fzonn0p1 13904	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℕ₀ → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
99	97, 61, 98	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
100		ccatws1len 14796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
101	100	ad4antr 745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
102	101	eqcomd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ((♯‘𝑑) + 1) = (♯‘(𝑑 ++ ⟨“𝑥”⟩)))
103		ccatws1cl 14792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
104	103	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
105	102, 104	wrdfd 14691	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩):(0..^((♯‘𝑑) + 1))⟶𝐴)
106	105	fdmd 6742	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → dom (𝑑 ++ ⟨“𝑥”⟩) = (0..^((♯‘𝑑) + 1)))
107	99, 106	eleqtrrd 2867	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ dom (𝑑 ++ ⟨“𝑥”⟩))
108		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ¬ 𝑑 = ∅)
109	108	neqned 2966	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ≠ ∅)
110		hasheq0 14534	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) = 0 ↔ 𝑑 = ∅))
111	110	necon3bid 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) ≠ 0 ↔ 𝑑 ≠ ∅))
112	111	biimpar 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0)
113	97, 109, 112	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ≠ 0)
114	107, 113	eldifsnd 4750	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
115		fvoveq1 7466	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)))
116		fveq2 6908	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
117	115, 116	breq12d 5119	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (♯‘𝑑) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
118	117	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ 𝑖 = (♯‘𝑑)) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
119	114, 118	rspcdv 3572	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
120	119	imp 412	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
121	47	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
122	49	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
123	121, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
124	113	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ≠ 0)
125		elnnne0 12647	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑑) ∈ ℕ ↔ ((♯‘𝑑) ∈ ℕ₀ ∧ (♯‘𝑑) ≠ 0))
126	123, 124, 125	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ)
127		fzo0end 13920	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑑) ∈ ℕ → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
128	126, 127	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
129		ccatval1 14749	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
130	121, 122, 128, 129	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
131	48	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑥 ∈ 𝐴)
132		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
133		ccats1val2 14803	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ (♯‘𝑑) = (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
134	121, 131, 132, 133	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
135	120, 130, 134	3brtr3d 5139	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘((♯‘𝑑) − 1)) < 𝑥)
136	96, 135	eqbrtrd 5130	. . . . . . . . . . 11 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) < 𝑥)
137	136	an42ds 1520	. . . . . . . . . 10 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) ∧ ¬ 𝑑 = ∅) → (lastS‘𝑑) < 𝑥)
138	137	ex 418	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (¬ 𝑑 = ∅ → (lastS‘𝑑) < 𝑥))
139	138	orrd 877	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥))
140		simpr 490	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜃)
141		chnind.8	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)
142	93, 94, 139, 140, 141	syl1111anc 854	. . . . . . 7 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜏)
143	142	ex 418	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏))
144	143	expl 463	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏)))
145	87	ralrimiva 3158	. . . . . . 7 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
146		fvoveq1 7466	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘(𝑖 − 1)) = (𝑑‘(𝑗 − 1)))
147		fveq2 6908	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘𝑖) = (𝑑‘𝑗))
148	146, 147	breq12d 5119	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → ((𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
149	148	cbvralvw 3244	. . . . . . 7 ⊢ (∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
150	145, 149	sylibr 237	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))
151	150	expl 463	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
152	144, 151	a2and 859	. . . 4 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
153	15, 24, 33, 42, 44, 152	wrdind 14899	. . 3 ⊢ (𝐶 ∈ Word 𝐴 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂))
154	153	imp 412	. 2 ⊢ ((𝐶 ∈ Word 𝐴 ∧ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) → 𝜂)
155	2, 3, 6, 154	syl12anc 850	1 ⊢ (𝜑 → 𝜂)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ⊆ wss 3900 ∖ cdif 4048 ∅c0 4281 {csn 4588 class class class wbr 5106 dom cdm 5655 ‘cfv 6558 (class class class)co 7443 0cc0 11227 1c1 11228 + caddc 11230 − cmin 11568 ℕcn 12362 ℕ₀cn0 12633 ℤcz 12720 ..^cfzo 13815 ♯chash 14501 Word cword 14685 lastSclsw 14734 ++ cconcat 14742 ⟨“cs1 14769 Chain cchn 18808

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-er 8745 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-nn 12363 df-n0 12634 df-xnn0 12707 df-z 12721 df-uz 12993 df-fz 13667 df-fzo 13816 df-hash 14502 df-word 14686 df-lsw 14735 df-concat 14743 df-s1 14770 df-substr 14817 df-pfx 14849 df-chn 18809

This theorem is used by: chnub 18825 fldext2chn 34430 chnerlem1 48097

W3C validator