Definition df-chn 32878

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 32877	. 2 class ( < Chain𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1533	. . . . . . 7 class 𝑛
6		c1 11150	. . . . . . 7 class 1
7		cmin 11485	. . . . . . 7 class −
8	5, 6, 7	co 7416	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1533	. . . . . 6 class 𝑐
11	8, 10	cfv 6546	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6546	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5145	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5674	. . . . 5 class dom 𝑐
15		cc0 11149	. . . . . 6 class 0
16	15	csn 4623	. . . . 5 class {0}
17	14, 16	cdif 3943	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3051	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14517	. . 3 class Word 𝐴
20	18, 9, 19	crab 3419	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1534	1 wff ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  32879