Definition df-chn 18652

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 18651	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1562	. . . . . . 7 class 𝑛
6		c1 11089	. . . . . . 7 class 1
7		cmin 11429	. . . . . . 7 class −
8	5, 6, 7	co 7400	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1562	. . . . . 6 class 𝑐
11	8, 10	cfv 6525	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6525	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5105	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5652	. . . . 5 class dom 𝑐
15		cc0 11088	. . . . . 6 class 0
16	15	csn 4585	. . . . 5 class {0}
17	14, 16	cdif 3904	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3079	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14540	. . 3 class Word 𝐴
20	18, 9, 19	crab 3417	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1563	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  18653  nfchnd  18657  chneq1  18658  chneq2  18659