Definition df-chn 18572

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 18571	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1541	. . . . . . 7 class 𝑛
6		c1 11039	. . . . . . 7 class 1
7		cmin 11377	. . . . . . 7 class −
8	5, 6, 7	co 7367	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1541	. . . . . 6 class 𝑐
11	8, 10	cfv 6498	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6498	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5085	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5631	. . . . 5 class dom 𝑐
15		cc0 11038	. . . . . 6 class 0
16	15	csn 4567	. . . . 5 class {0}
17	14, 16	cdif 3886	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3051	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14475	. . 3 class Word 𝐴
20	18, 9, 19	crab 3389	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1542	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  18573  nfchnd  18577  chneq1  18578  chneq2  18579