Definition df-chn

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)

	Ref	Expression
Assertion	df-chn	⊢ ( < Chain 𝐴 ) = { 𝑐 ∈ Word 𝐴 ∣ ∀ 𝑛 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑛 − 1 ) ) < ( 𝑐 ‘ 𝑛 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c.lt	⊢ <
1		cA	⊢ 𝐴
2	1 0	cchn	⊢ ( < Chain 𝐴 )
3		vc	⊢ 𝑐
4	1	cword	⊢ Word 𝐴
5		vn	⊢ 𝑛
6	3	cv	⊢ 𝑐
7	6	cdm	⊢ dom 𝑐
8		cc0	⊢ 0
9	8	csn	⊢ { 0 }
10	7 9	cdif	⊢ ( dom 𝑐 ∖ { 0 } )
11	5	cv	⊢ 𝑛
12		cmin	⊢ −
13		c1	⊢ 1
14	11 13 12	co	⊢ ( 𝑛 − 1 )
15	14 6	cfv	⊢ ( 𝑐 ‘ ( 𝑛 − 1 ) )
16	11 6	cfv	⊢ ( 𝑐 ‘ 𝑛 )
17	15 16 0	wbr	⊢ ( 𝑐 ‘ ( 𝑛 − 1 ) ) < ( 𝑐 ‘ 𝑛 )
18	17 5 10	wral	⊢ ∀ 𝑛 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑛 − 1 ) ) < ( 𝑐 ‘ 𝑛 )
19	18 3 4	crab	⊢ { 𝑐 ∈ Word 𝐴 ∣ ∀ 𝑛 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑛 − 1 ) ) < ( 𝑐 ‘ 𝑛 ) }
20	2 19	wceq	⊢ ( < Chain 𝐴 ) = { 𝑐 ∈ Word 𝐴 ∣ ∀ 𝑛 ∈ ( dom 𝑐 ∖ { 0 } ) ( 𝑐 ‘ ( 𝑛 − 1 ) ) < ( 𝑐 ‘ 𝑛 ) }