Definition df-chn 18663

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 18662	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1569	. . . . . . 7 class 𝑛
6		c1 11102	. . . . . . 7 class 1
7		cmin 11442	. . . . . . 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 6538	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6538	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5110	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5663	. . . . 5 class dom 𝑐
15		cc0 11101	. . . . . 6 class 0
16	15	csn 4590	. . . . 5 class {0}
17	14, 16	cdif 3903	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3079	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14552	. . 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 referenced by:  ischn  18664  nfchnd  18668  chneq1  18669  chneq2  18670