Definition df-chn 18700

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 18699	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1569	. . . . . . 7 class 𝑛
6		c1 11129	. . . . . . 7 class 1
7		cmin 11469	. . . . . . 7 class −
8	5, 6, 7	co 7417	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1569	. . . . . 6 class 𝑐
11	8, 10	cfv 6537	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6537	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5107	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5659	. . . . 5 class dom 𝑐
15		cc0 11128	. . . . . 6 class 0
16	15	csn 4587	. . . . 5 class {0}
17	14, 16	cdif 3899	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3078	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14582	. . 3 class Word 𝐴
20	18, 9, 19	crab 3414	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1570	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is used by:  ischn  18701  nfchnd  18705  chneq1  18706  chneq2  18707