Definition df-chn 18570

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 18569	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1546	. . . . . . 7 class 𝑛
6		c1 11037	. . . . . . 7 class 1
7		cmin 11375	. . . . . . 7 class −
8	5, 6, 7	co 7363	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1546	. . . . . 6 class 𝑐
11	8, 10	cfv 6492	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6492	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5079	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5625	. . . . 5 class dom 𝑐
15		cc0 11036	. . . . . 6 class 0
16	15	csn 4562	. . . . 5 class {0}
17	14, 16	cdif 3887	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3054	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14473	. . 3 class Word 𝐴
20	18, 9, 19	crab 3392	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1547	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  18571  nfchnd  18575  chneq1  18576  chneq2  18577