Definition df-chn 18514

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 18513	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1540	. . . . . . 7 class 𝑛
6		c1 11014	. . . . . . 7 class 1
7		cmin 11351	. . . . . . 7 class −
8	5, 6, 7	co 7352	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1540	. . . . . 6 class 𝑐
11	8, 10	cfv 6486	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6486	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5093	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5619	. . . . 5 class dom 𝑐
15		cc0 11013	. . . . . 6 class 0
16	15	csn 4575	. . . . 5 class {0}
17	14, 16	cdif 3895	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3048	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14422	. . 3 class Word 𝐴
20	18, 9, 19	crab 3396	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1541	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  18515  nfchnd  18519  chneq1  18520  chneq2  18521