Definition df-chn 32931

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 32930	. 2 class ( < Chain𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1539	. . . . . . 7 class 𝑛
6		c1 11069	. . . . . . 7 class 1
7		cmin 11405	. . . . . . 7 class −
8	5, 6, 7	co 7387	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1539	. . . . . 6 class 𝑐
11	8, 10	cfv 6511	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6511	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5107	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5638	. . . . 5 class dom 𝑐
15		cc0 11068	. . . . . 6 class 0
16	15	csn 4589	. . . . 5 class {0}
17	14, 16	cdif 3911	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3044	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14478	. . 3 class Word 𝐴
20	18, 9, 19	crab 3405	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1540	1 wff ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  32932