Definition df-chn 18809

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 18808	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1569	. . . . . . 7 class 𝑛
6		c1 11228	. . . . . . 7 class 1
7		cmin 11568	. . . . . . 7 class −
8	5, 6, 7	co 7443	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1569	. . . . . 6 class 𝑐
11	8, 10	cfv 6558	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6558	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5106	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5655	. . . . 5 class dom 𝑐
15		cc0 11227	. . . . . 6 class 0
16	15	csn 4588	. . . . 5 class {0}
17	14, 16	cdif 4048	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3080	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14685	. . 3 class Word 𝐴
20	18, 9, 19	crab 3416	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1570	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is used by:  ischn  18810  nfchnd  18814  chneq1  18815  chneq2  18816