Definition df-chn 18760

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 18759	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1569	. . . . . . 7 class 𝑛
6		c1 11182	. . . . . . 7 class 1
7		cmin 11522	. . . . . . 7 class −
8	5, 6, 7	co 7412	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1569	. . . . . 6 class 𝑐
11	8, 10	cfv 6531	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6531	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5103	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5651	. . . . 5 class dom 𝑐
15		cc0 11181	. . . . . 6 class 0
16	15	csn 4584	. . . . 5 class {0}
17	14, 16	cdif 3896	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3077	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14638	. . 3 class Word 𝐴
20	18, 9, 19	crab 3413	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1570	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is used by:  ischn  18761  nfchnd  18765  chneq1  18766  chneq2  18767