Definition df-chn 18621

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 18620	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1558	. . . . . . 7 class 𝑛
6		c1 11071	. . . . . . 7 class 1
7		cmin 11411	. . . . . . 7 class −
8	5, 6, 7	co 7392	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1558	. . . . . 6 class 𝑐
11	8, 10	cfv 6517	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6517	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5099	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5645	. . . . 5 class dom 𝑐
15		cc0 11070	. . . . . 6 class 0
16	15	csn 4581	. . . . 5 class {0}
17	14, 16	cdif 3901	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3075	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14523	. . 3 class Word 𝐴
20	18, 9, 19	crab 3413	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1559	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  18622  nfchnd  18626  chneq1  18627  chneq2  18628