Definition df-chn 32978

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 32977	. 2 class ( < Chain𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1536	. . . . . . 7 class 𝑛
6		c1 11185	. . . . . . 7 class 1
7		cmin 11520	. . . . . . 7 class −
8	5, 6, 7	co 7448	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1536	. . . . . 6 class 𝑐
11	8, 10	cfv 6573	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6573	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5166	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5700	. . . . 5 class dom 𝑐
15		cc0 11184	. . . . . 6 class 0
16	15	csn 4648	. . . . 5 class {0}
17	14, 16	cdif 3973	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3067	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14562	. . 3 class Word 𝐴
20	18, 9, 19	crab 3443	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1537	1 wff ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  32979