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 32944

Description: Induction over a chain. See nnind 12211 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 32940	. 2 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
3		id 22	. 2 ⊢ (𝜑 → 𝜑)
4		ischn 32939	. . . 4 ⊢ (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
5	1, 4	sylib 218	. . 3 ⊢ (𝜑 → (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
6	5	simprd 495	. 2 ⊢ (𝜑 → ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))
7		dmeq 5870	. . . . . . . 8 ⊢ (𝑐 = ∅ → dom 𝑐 = dom ∅)
8	7	difeq1d 4091	. . . . . . 7 ⊢ (𝑐 = ∅ → (dom 𝑐 ∖ {0}) = (dom ∅ ∖ {0}))
9		fveq1 6860	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘(𝑖 − 1)) = (∅‘(𝑖 − 1)))
10		fveq1 6860	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘𝑖) = (∅‘𝑖))
11	9, 10	breq12d 5123	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (∅‘(𝑖 − 1)) < (∅‘𝑖)))
12	8, 11	raleqbidv 3321	. . . . . 6 ⊢ (𝑐 = ∅ → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)))
13	12	anbi2d 630	. . . . 5 ⊢ (𝑐 = ∅ → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖))))
14		chnind.1	. . . . 5 ⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))
15	13, 14	imbi12d 344	. . . 4 ⊢ (𝑐 = ∅ → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)))
16		dmeq 5870	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → dom 𝑐 = dom 𝑑)
17	16	difeq1d 4091	. . . . . . 7 ⊢ (𝑐 = 𝑑 → (dom 𝑐 ∖ {0}) = (dom 𝑑 ∖ {0}))
18		fveq1 6860	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘(𝑖 − 1)) = (𝑑‘(𝑖 − 1)))
19		fveq1 6860	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑖) = (𝑑‘𝑖))
20	18, 19	breq12d 5123	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
21	17, 20	raleqbidv 3321	. . . . . 6 ⊢ (𝑐 = 𝑑 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
22	21	anbi2d 630	. . . . 5 ⊢ (𝑐 = 𝑑 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))))
23		chnind.2	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))
24	22, 23	imbi12d 344	. . . 4 ⊢ (𝑐 = 𝑑 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃)))
25		dmeq 5870	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → dom 𝑐 = dom (𝑑 ++ ⟨“𝑥”⟩))
26	25	difeq1d 4091	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (dom 𝑐 ∖ {0}) = (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
27		fveq1 6860	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)))
28		fveq1 6860	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))
29	27, 28	breq12d 5123	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
30	26, 29	raleqbidv 3321	. . . . . 6 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
31	30	anbi2d 630	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))))
32		chnind.3	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))
33	31, 32	imbi12d 344	. . . 4 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
34		dmeq 5870	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → dom 𝑐 = dom 𝐶)
35	34	difeq1d 4091	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (dom 𝑐 ∖ {0}) = (dom 𝐶 ∖ {0}))
36		fveq1 6860	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘(𝑖 − 1)) = (𝐶‘(𝑖 − 1)))
37		fveq1 6860	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑖) = (𝐶‘𝑖))
38	36, 37	breq12d 5123	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
39	35, 38	raleqbidv 3321	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
40	39	anbi2d 630	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) ↔ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))))
41		chnind.4	. . . . 5 ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))
42	40, 41	imbi12d 344	. . . 4 ⊢ (𝑐 = 𝐶 → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖)) → 𝜓) ↔ ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂)))
43		chnind.7	. . . . 5 ⊢ (𝜑 → 𝜒)
44	43	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)
45		simpllr 775	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜑)
46		simp-4l 782	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
47		simpll 766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑑 ∈ Word 𝐴)
48		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑥 ∈ 𝐴)
49	48	s1cld 14575	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → ⟨“𝑥”⟩ ∈ Word 𝐴)
50	47, 49	ccatdmss 32878	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → dom 𝑑 ⊆ dom (𝑑 ++ ⟨“𝑥”⟩))
51	50	ssdifd 4111	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → (dom 𝑑 ∖ {0}) ⊆ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
52	51	sselda 3949	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → 𝑗 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
53		fvoveq1 7413	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)))
54		fveq2 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
55	53, 54	breq12d 5123	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
56	55	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ 𝑖 = 𝑗) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
57	52, 56	rspcdv 3583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
58	57	imp 406	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
59		simp-4l 782	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
60	49	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
61		lencl 14505	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈ ℕ₀)
62	59, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
63	62	nn0zd 12562	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℤ)
64		fzossrbm1 13656	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℤ → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
65	63, 64	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
66		fzossz 13647	. . . . . . . . . . . . . . . . . . 19 ⊢ (0..^(♯‘𝑑)) ⊆ ℤ
67		simplr 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (dom 𝑑 ∖ {0}))
68	67	eldifad 3929	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ dom 𝑑)
69		eqidd 2731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
70	69, 59	wrdfd 14491	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑:(0..^(♯‘𝑑))⟶𝐴)
71	70	fdmd 6701	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → dom 𝑑 = (0..^(♯‘𝑑)))
72	68, 71	eleqtrd 2831	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (0..^(♯‘𝑑)))
73	66, 72	sselid 3947	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ ℤ)
74		eldifsni 4757	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (dom 𝑑 ∖ {0}) → 𝑗 ≠ 0)
75	67, 74	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ≠ 0)
76		fzo1fzo0n0 13683	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 ∈ (0..^(♯‘𝑑)) ∧ 𝑗 ≠ 0))
77	72, 75, 76	sylanbrc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (1..^(♯‘𝑑)))
78		elfzom1b 13734	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) → (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1))))
79	78	biimpa 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) ∧ 𝑗 ∈ (1..^(♯‘𝑑))) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
80	73, 63, 77, 79	syl21anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
81	65, 80	sseldd 3950	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^(♯‘𝑑)))
82		ccatval1 14549	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ (𝑗 − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
83	59, 60, 81, 82	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
84		ccatval1 14549	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ 𝑗 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
85	59, 60, 72, 84	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
86	58, 83, 85	3brtr3d 5141	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
87	86	an32s 652	. . . . . . . . . . . . 13 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
88	87	adantllr 719	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
89	88	ralrimiva 3126	. . . . . . . . . . 11 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
90	89	an32s 652	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
91		ischn 32939	. . . . . . . . . 10 ⊢ (𝑑 ∈ ( < Chain𝐴) ↔ (𝑑 ∈ Word 𝐴 ∧ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
92	46, 90, 91	sylanbrc 583	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ ( < Chain𝐴))
93	45, 92	jca 511	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)))
94		simp-4r 783	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑥 ∈ 𝐴)
95		lsw 14536	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ Word 𝐴 → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
96	95	ad5antr 734	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
97		simp-4l 782	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
98		fzonn0p1 13710	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℕ₀ → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
99	97, 61, 98	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
100		ccatws1len 14592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
101	100	ad4antr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
102	101	eqcomd 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ((♯‘𝑑) + 1) = (♯‘(𝑑 ++ ⟨“𝑥”⟩)))
103		ccatws1cl 14588	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
104	103	ad3antrrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
105	102, 104	wrdfd 14491	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩):(0..^((♯‘𝑑) + 1))⟶𝐴)
106	105	fdmd 6701	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → dom (𝑑 ++ ⟨“𝑥”⟩) = (0..^((♯‘𝑑) + 1)))
107	99, 106	eleqtrrd 2832	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ dom (𝑑 ++ ⟨“𝑥”⟩))
108		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ¬ 𝑑 = ∅)
109	108	neqned 2933	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ≠ ∅)
110		hasheq0 14335	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) = 0 ↔ 𝑑 = ∅))
111	110	necon3bid 2970	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) ≠ 0 ↔ 𝑑 ≠ ∅))
112	111	biimpar 477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0)
113	97, 109, 112	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ≠ 0)
114	107, 113	eldifsnd 4754	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
115		fvoveq1 7413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)))
116		fveq2 6861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
117	115, 116	breq12d 5123	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (♯‘𝑑) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
118	117	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ 𝑖 = (♯‘𝑑)) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
119	114, 118	rspcdv 3583	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
120	119	imp 406	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
121	47	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
122	49	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
123	121, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
124	113	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ≠ 0)
125		elnnne0 12463	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑑) ∈ ℕ ↔ ((♯‘𝑑) ∈ ℕ₀ ∧ (♯‘𝑑) ≠ 0))
126	123, 124, 125	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ)
127		fzo0end 13726	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑑) ∈ ℕ → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
128	126, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
129		ccatval1 14549	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
130	121, 122, 128, 129	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
131	48	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑥 ∈ 𝐴)
132		eqidd 2731	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
133		ccats1val2 14599	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ (♯‘𝑑) = (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
134	121, 131, 132, 133	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
135	120, 130, 134	3brtr3d 5141	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘((♯‘𝑑) − 1)) < 𝑥)
136	96, 135	eqbrtrd 5132	. . . . . . . . . . 11 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) < 𝑥)
137	136	an42ds 32386	. . . . . . . . . 10 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) ∧ ¬ 𝑑 = ∅) → (lastS‘𝑑) < 𝑥)
138	137	ex 412	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (¬ 𝑑 = ∅ → (lastS‘𝑑) < 𝑥))
139	138	orrd 863	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥))
140		simpr 484	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜃)
141		chnind.8	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)
142	93, 94, 139, 140, 141	syl1111anc 840	. . . . . . 7 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜏)
143	142	ex 412	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏))
144	143	expl 457	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏)))
145	87	ralrimiva 3126	. . . . . . 7 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
146		fvoveq1 7413	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘(𝑖 − 1)) = (𝑑‘(𝑗 − 1)))
147		fveq2 6861	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘𝑖) = (𝑑‘𝑗))
148	146, 147	breq12d 5123	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → ((𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
149	148	cbvralvw 3216	. . . . . . 7 ⊢ (∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
150	145, 149	sylibr 234	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))
151	150	expl 457	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
152	144, 151	a2and 845	. . . 4 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
153	15, 24, 33, 42, 44, 152	wrdind 14694	. . 3 ⊢ (𝐶 ∈ Word 𝐴 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂))
154	153	imp 406	. 2 ⊢ ((𝐶 ∈ Word 𝐴 ∧ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) → 𝜂)
155	2, 3, 6, 154	syl12anc 836	1 ⊢ (𝜑 → 𝜂)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ∖ cdif 3914 ⊆ wss 3917 ∅c0 4299 {csn 4592 class class class wbr 5110 dom cdm 5641 ‘cfv 6514 (class class class)co 7390 0cc0 11075 1c1 11076 + caddc 11078 − cmin 11412 ℕcn 12193 ℕ₀cn0 12449 ℤcz 12536 ..^cfzo 13622 ♯chash 14302 Word cword 14485 lastSclsw 14534 ++ cconcat 14542 ⟨“cs1 14567 Chaincchn 32937

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-er 8674 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-nn 12194 df-n0 12450 df-xnn0 12523 df-z 12537 df-uz 12801 df-fz 13476 df-fzo 13623 df-hash 14303 df-word 14486 df-lsw 14535 df-concat 14543 df-s1 14568 df-substr 14613 df-pfx 14643 df-chn 32938

This theorem is referenced by: chnub 32945 fldext2chn 33725

W3C validator