Definition df-chn 18529

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 18528	. 2 class ( < Chain 𝐴)
4		vn	. . . . . . . 8 setvar 𝑛
5	4	cv 1540	. . . . . . 7 class 𝑛
6		c1 11027	. . . . . . 7 class 1
7		cmin 11364	. . . . . . 7 class −
8	5, 6, 7	co 7358	. . . . . 6 class (𝑛 − 1)
9		vc	. . . . . . 7 setvar 𝑐
10	9	cv 1540	. . . . . 6 class 𝑐
11	8, 10	cfv 6492	. . . . 5 class (𝑐‘(𝑛 − 1))
12	5, 10	cfv 6492	. . . . 5 class (𝑐‘𝑛)
13	11, 12, 2	wbr 5098	. . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
14	10	cdm 5624	. . . . 5 class dom 𝑐
15		cc0 11026	. . . . . 6 class 0
16	15	csn 4580	. . . . 5 class {0}
17	14, 16	cdif 3898	. . . 4 class (dom 𝑐 ∖ {0})
18	13, 4, 17	wral 3051	. . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)
19	1	cword 14436	. . 3 class Word 𝐴
20	18, 9, 19	crab 3399	. 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
21	3, 20	wceq 1541	1 wff ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}

This definition is referenced by:  ischn  18530  nfchnd  18534  chneq1  18535  chneq2  18536