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 18678

Description: Induction over a chain. See nnind 12252 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 18665	. 2 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
3		id 23	. 2 ⊢ (𝜑 → 𝜑)
4		ischn 18664	. . . 4 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
5	1, 4	sylib 221	. . 3 ⊢ (𝜑 → (𝐶 ∈ Word 𝐴 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
6	5	simprd 500	. 2 ⊢ (𝜑 → ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))
7		dmeq 5895	. . . . . . . 8 ⊢ (𝑐 = ∅ → dom 𝑐 = dom ∅)
8	7	difeq1d 4081	. . . . . . 7 ⊢ (𝑐 = ∅ → (dom 𝑐 ∖ {0}) = (dom ∅ ∖ {0}))
9		fveq1 6882	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘(𝑖 − 1)) = (∅‘(𝑖 − 1)))
10		fveq1 6882	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑐‘𝑖) = (∅‘𝑖))
11	9, 10	breq12d 5123	. . . . . . 7 ⊢ (𝑐 = ∅ → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (∅‘(𝑖 − 1)) < (∅‘𝑖)))
12	8, 11	raleqbidv 3338	. . . . . 6 ⊢ (𝑐 = ∅ → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)))
13	12	anbi2d 641	. . . . 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 5895	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → dom 𝑐 = dom 𝑑)
17	16	difeq1d 4081	. . . . . . 7 ⊢ (𝑐 = 𝑑 → (dom 𝑐 ∖ {0}) = (dom 𝑑 ∖ {0}))
18		fveq1 6882	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘(𝑖 − 1)) = (𝑑‘(𝑖 − 1)))
19		fveq1 6882	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑖) = (𝑑‘𝑖))
20	18, 19	breq12d 5123	. . . . . . 7 ⊢ (𝑐 = 𝑑 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
21	17, 20	raleqbidv 3338	. . . . . 6 ⊢ (𝑐 = 𝑑 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
22	21	anbi2d 641	. . . . 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 5895	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → dom 𝑐 = dom (𝑑 ++ ⟨“𝑥”⟩))
26	25	difeq1d 4081	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (dom 𝑐 ∖ {0}) = (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
27		fveq1 6882	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)))
28		fveq1 6882	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))
29	27, 28	breq12d 5123	. . . . . . 7 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
30	26, 29	raleqbidv 3338	. . . . . 6 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)))
31	30	anbi2d 641	. . . . 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 5895	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → dom 𝑐 = dom 𝐶)
35	34	difeq1d 4081	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (dom 𝑐 ∖ {0}) = (dom 𝐶 ∖ {0}))
36		fveq1 6882	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘(𝑖 − 1)) = (𝐶‘(𝑖 − 1)))
37		fveq1 6882	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑖) = (𝐶‘𝑖))
38	36, 37	breq12d 5123	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ (𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
39	35, 38	raleqbidv 3338	. . . . . 6 ⊢ (𝑐 = 𝐶 → (∀𝑖 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑖 − 1)) < (𝑐‘𝑖) ↔ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)))
40	39	anbi2d 641	. . . . 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 485	. . . 4 ⊢ ((𝜑 ∧ ∀𝑖 ∈ (dom ∅ ∖ {0})(∅‘(𝑖 − 1)) < (∅‘𝑖)) → 𝜒)
45		simpllr 787	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜑)
46		simp-4l 794	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
47		simpll 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑑 ∈ Word 𝐴)
48		simplr 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → 𝑥 ∈ 𝐴)
49	48	s1cld 14643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → ⟨“𝑥”⟩ ∈ Word 𝐴)
50	47, 49	ccatdmss 14621	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → dom 𝑑 ⊆ dom (𝑑 ++ ⟨“𝑥”⟩))
51	50	ssdifd 4100	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) → (dom 𝑑 ∖ {0}) ⊆ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
52	51	sselda 3938	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → 𝑗 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
53		fvoveq1 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)))
54		fveq2 6883	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
55	53, 54	breq12d 5123	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
56	55	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ 𝑖 = 𝑗) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
57	52, 56	rspcdv 3574	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗)))
58	57	imp 411	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
59		simp-4l 794	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
60	49	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
61		lencl 14572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈ ℕ₀)
62	59, 61	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
63	62	nn0zd 12617	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℤ)
64		fzossrbm1 13719	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℤ → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
65	63, 64	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (0..^((♯‘𝑑) − 1)) ⊆ (0..^(♯‘𝑑)))
66		fzossz 13710	. . . . . . . . . . . . . . . . . . 19 ⊢ (0..^(♯‘𝑑)) ⊆ ℤ
67		simplr 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (dom 𝑑 ∖ {0}))
68	67	eldifad 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ dom 𝑑)
69		eqidd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
70	69, 59	wrdfd 14558	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑:(0..^(♯‘𝑑))⟶𝐴)
71	70	fdmd 6718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → dom 𝑑 = (0..^(♯‘𝑑)))
72	68, 71	eleqtrd 2865	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (0..^(♯‘𝑑)))
73	66, 72	sselid 3936	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ ℤ)
74		eldifsni 4759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (dom 𝑑 ∖ {0}) → 𝑗 ≠ 0)
75	67, 74	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ≠ 0)
76		fzo1fzo0n0 13746	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 ∈ (0..^(♯‘𝑑)) ∧ 𝑗 ≠ 0))
77	72, 75, 76	sylanbrc 594	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑗 ∈ (1..^(♯‘𝑑)))
78		elfzom1b 13797	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) → (𝑗 ∈ (1..^(♯‘𝑑)) ↔ (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1))))
79	78	biimpa 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑗 ∈ ℤ ∧ (♯‘𝑑) ∈ ℤ) ∧ 𝑗 ∈ (1..^(♯‘𝑑))) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
80	73, 63, 77, 79	syl21anc 850	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^((♯‘𝑑) − 1)))
81	65, 80	sseldd 3939	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑗 − 1) ∈ (0..^(♯‘𝑑)))
82		ccatval1 14616	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ (𝑗 − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
83	59, 60, 81, 82	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑗 − 1)) = (𝑑‘(𝑗 − 1)))
84		ccatval1 14616	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ 𝑗 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
85	59, 60, 72, 84	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = (𝑑‘𝑗))
86	58, 83, 85	3brtr3d 5143	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
87	86	an32s 664	. . . . . . . . . . . . 13 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
88	87	adantllr 731	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝑗 ∈ (dom 𝑑 ∖ {0})) → (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
89	88	ralrimiva 3157	. . . . . . . . . . 11 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
90	89	an32s 664	. . . . . . . . . 10 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
91		ischn 18664	. . . . . . . . . 10 ⊢ (𝑑 ∈ ( < Chain 𝐴) ↔ (𝑑 ∈ Word 𝐴 ∧ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
92	46, 90, 91	sylanbrc 594	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑑 ∈ ( < Chain 𝐴))
93	45, 92	jca 520	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)))
94		simp-4r 795	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝑥 ∈ 𝐴)
95		lsw 14603	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ Word 𝐴 → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
96	95	ad5antr 746	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) = (𝑑‘((♯‘𝑑) − 1)))
97		simp-4l 794	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ∈ Word 𝐴)
98		fzonn0p1 13773	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑑) ∈ ℕ₀ → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
99	97, 61, 98	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (0..^((♯‘𝑑) + 1)))
100		ccatws1len 14660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
101	100	ad4antr 744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
102	101	eqcomd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ((♯‘𝑑) + 1) = (♯‘(𝑑 ++ ⟨“𝑥”⟩)))
103		ccatws1cl 14656	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
104	103	ad3antrrr 742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩) ∈ Word 𝐴)
105	102, 104	wrdfd 14558	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (𝑑 ++ ⟨“𝑥”⟩):(0..^((♯‘𝑑) + 1))⟶𝐴)
106	105	fdmd 6718	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → dom (𝑑 ++ ⟨“𝑥”⟩) = (0..^((♯‘𝑑) + 1)))
107	99, 106	eleqtrrd 2866	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ dom (𝑑 ++ ⟨“𝑥”⟩))
108		simplr 780	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → ¬ 𝑑 = ∅)
109	108	neqned 2965	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → 𝑑 ≠ ∅)
110		hasheq0 14401	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) = 0 ↔ 𝑑 = ∅))
111	110	necon3bid 3002	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Word 𝐴 → ((♯‘𝑑) ≠ 0 ↔ 𝑑 ≠ ∅))
112	111	biimpar 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑑 ≠ ∅) → (♯‘𝑑) ≠ 0)
113	97, 109, 112	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ≠ 0)
114	107, 113	eldifsnd 4756	. . . . . . . . . . . . . . 15 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (♯‘𝑑) ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0}))
115		fvoveq1 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) = ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)))
116		fveq2 6883	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (♯‘𝑑) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
117	115, 116	breq12d 5123	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (♯‘𝑑) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
118	117	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ 𝑖 = (♯‘𝑑)) → (((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
119	114, 118	rspcdv 3574	. . . . . . . . . . . . . 14 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) → (∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑))))
120	119	imp 411	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)))
121	47	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑑 ∈ Word 𝐴)
122	49	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ⟨“𝑥”⟩ ∈ Word 𝐴)
123	121, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ₀)
124	113	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ≠ 0)
125		elnnne0 12519	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑑) ∈ ℕ ↔ ((♯‘𝑑) ∈ ℕ₀ ∧ (♯‘𝑑) ≠ 0))
126	123, 124, 125	sylanbrc 594	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) ∈ ℕ)
127		fzo0end 13789	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑑) ∈ ℕ → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
128	126, 127	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑)))
129		ccatval1 14616	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ ⟨“𝑥”⟩ ∈ Word 𝐴 ∧ ((♯‘𝑑) − 1) ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
130	121, 122, 128, 129	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘((♯‘𝑑) − 1)) = (𝑑‘((♯‘𝑑) − 1)))
131	48	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝑥 ∈ 𝐴)
132		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (♯‘𝑑) = (♯‘𝑑))
133		ccats1val2 14667	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ (♯‘𝑑) = (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
134	121, 131, 132, 133	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ((𝑑 ++ ⟨“𝑥”⟩)‘(♯‘𝑑)) = 𝑥)
135	120, 130, 134	3brtr3d 5143	. . . . . . . . . . . 12 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝑑‘((♯‘𝑑) − 1)) < 𝑥)
136	96, 135	eqbrtrd 5134	. . . . . . . . . . 11 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ¬ 𝑑 = ∅) ∧ 𝜃) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (lastS‘𝑑) < 𝑥)
137	136	an42ds 1520	. . . . . . . . . 10 ⊢ ((((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) ∧ ¬ 𝑑 = ∅) → (lastS‘𝑑) < 𝑥)
138	137	ex 417	. . . . . . . . 9 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (¬ 𝑑 = ∅ → (lastS‘𝑑) < 𝑥))
139	138	orrd 876	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥))
140		simpr 489	. . . . . . . 8 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜃)
141		chnind.8	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)
142	93, 94, 139, 140, 141	syl1111anc 853	. . . . . . 7 ⊢ (((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) ∧ 𝜃) → 𝜏)
143	142	ex 417	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏))
144	143	expl 462	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → (𝜃 → 𝜏)))
145	87	ralrimiva 3157	. . . . . . 7 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
146		fvoveq1 7435	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘(𝑖 − 1)) = (𝑑‘(𝑗 − 1)))
147		fveq2 6883	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (𝑑‘𝑖) = (𝑑‘𝑗))
148	146, 147	breq12d 5123	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → ((𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ (𝑑‘(𝑗 − 1)) < (𝑑‘𝑗)))
149	148	cbvralvw 3243	. . . . . . 7 ⊢ (∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖) ↔ ∀𝑗 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑗 − 1)) < (𝑑‘𝑗))
150	145, 149	sylibr 237	. . . . . 6 ⊢ ((((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝜑) ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖))
151	150	expl 462	. . . . 5 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)))
152	144, 151	a2and 858	. . . 4 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝜑 ∧ ∀𝑖 ∈ (dom 𝑑 ∖ {0})(𝑑‘(𝑖 − 1)) < (𝑑‘𝑖)) → 𝜃) → ((𝜑 ∧ ∀𝑖 ∈ (dom (𝑑 ++ ⟨“𝑥”⟩) ∖ {0})((𝑑 ++ ⟨“𝑥”⟩)‘(𝑖 − 1)) < ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖)) → 𝜏)))
153	15, 24, 33, 42, 44, 152	wrdind 14761	. . 3 ⊢ (𝐶 ∈ Word 𝐴 → ((𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖)) → 𝜂))
154	153	imp 411	. 2 ⊢ ((𝐶 ∈ Word 𝐴 ∧ (𝜑 ∧ ∀𝑖 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑖 − 1)) < (𝐶‘𝑖))) → 𝜂)
155	2, 3, 6, 154	syl12anc 849	1 ⊢ (𝜑 → 𝜂)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∖ cdif 3903 ⊆ wss 3906 ∅c0 4287 {csn 4590 class class class wbr 5110 dom cdm 5663 ‘cfv 6538 (class class class)co 7412 0cc0 11101 1c1 11102 + caddc 11104 − cmin 11442 ℕcn 12234 ℕ₀cn0 12505 ℤcz 12592 ..^cfzo 13684 ♯chash 14368 Word cword 14552 lastSclsw 14601 ++ cconcat 14609 ⟨“cs1 14635 Chain cchn 18662

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-card 9926 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-n0 12506 df-xnn0 12579 df-z 12593 df-uz 12864 df-fz 13537 df-fzo 13685 df-hash 14369 df-word 14553 df-lsw 14602 df-concat 14610 df-s1 14636 df-substr 14681 df-pfx 14711 df-chn 18663

This theorem is referenced by: chnub 18679 fldext2chn 34096 chnerlem1 47578

W3C validator