Definition df-chn 18785

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 18784	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1568	. . . . . . 7 class 𝑛
6		c1 11204	. . . . . . 7 class 1
7		cmin 11544	. . . . . . 7 class −
8	5, 6, 7	co 7420	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1568	. . . . . 6 class 𝑐
11	8, 10	cfv 6538	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6538	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5102	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5650	. . . . 5 class dom 𝑐
15		cc0 11203	. . . . . 6 class 0
16	15	csn 4584	. . . . 5 class {0}
17	14, 16	cdif 4045	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3076	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14661	. . 3 class Word 𝐴
20	18, 9, 19	crab 3412	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1569	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is used by:  ischn  18786  nfchnd  18790  chneq1  18791  chneq2  18792