Definition df-chn 18522

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 18521	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1540	. . . . . . 7 class 𝑛
6		c1 11017	. . . . . . 7 class 1
7		cmin 11354	. . . . . . 7 class −
8	5, 6, 7	co 7355	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1540	. . . . . 6 class 𝑐
11	8, 10	cfv 6489	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6489	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5095	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5621	. . . . 5 class dom 𝑐
15		cc0 11016	. . . . . 6 class 0
16	15	csn 4577	. . . . 5 class {0}
17	14, 16	cdif 3896	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3049	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14430	. . 3 class Word 𝐴
20	18, 9, 19	crab 3397	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1541	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  18523  nfchnd  18527  chneq1  18528  chneq2  18529