Definition df-chn 18687

Description: Define the class of (finite) chains. A chain is defined to be a sequence of objects, where each object is less than the next one in the sequence. The term "chain" is usually used in order theory. In the context of algebra, chains are often called "towers", for example for fields, or "series", for example for subgroup or subnormal series. (Contributed by Thierry Arnoux, 19-Jun-2025.)

Assertion

Ref	Expression
df-chn	⊢ ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

Distinct variable groups:   𝐴,𝑐,𝑛   < ,𝑐,𝑛

Detailed syntax breakdown of Definition df-chn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		c.lt	. . 3 class <
3	1, 2	cchn 18686	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1569	. . . . . . 7 class 𝑛
6		c1 11119	. . . . . . 7 class 1
7		cmin 11459	. . . . . . 7 class −
8	5, 6, 7	co 7423	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1569	. . . . . 6 class 𝑐
11	8, 10	cfv 6543	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6543	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5114	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5666	. . . . 5 class dom 𝑐
15		cc0 11118	. . . . . 6 class 0
16	15	csn 4594	. . . . 5 class {0}
17	14, 16	cdif 3905	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3082	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14570	. . 3 class Word 𝐴
20	18, 9, 19	crab 3419	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1570	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is used by:  ischn  18688  nfchnd  18692  chneq1  18693  chneq2  18694