Definition df-chn 18512

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 18511	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1540	. . . . . . 7 class 𝑛
6		c1 11007	. . . . . . 7 class 1
7		cmin 11344	. . . . . . 7 class −
8	5, 6, 7	co 7346	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1540	. . . . . 6 class 𝑐
11	8, 10	cfv 6481	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6481	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5091	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5616	. . . . 5 class dom 𝑐
15		cc0 11006	. . . . . 6 class 0
16	15	csn 4576	. . . . 5 class {0}
17	14, 16	cdif 3899	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3047	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14420	. . 3 class Word 𝐴
20	18, 9, 19	crab 3395	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1541	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  18513  nfchnd  18517  chneq1  18518  chneq2  18519