Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-chn Structured version   Visualization version   GIF version

Definition df-chn 32980
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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 c.lt . . 3 class <
31, 2cchn 32979 . 2 class ( < Chain𝐴)
4 vn . . . . . . . 8 setvar 𝑛
54cv 1536 . . . . . . 7 class 𝑛
6 c1 11154 . . . . . . 7 class 1
7 cmin 11490 . . . . . . 7 class
85, 6, 7co 7431 . . . . . 6 class (𝑛 − 1)
9 vc . . . . . . 7 setvar 𝑐
109cv 1536 . . . . . 6 class 𝑐
118, 10cfv 6563 . . . . 5 class (𝑐‘(𝑛 − 1))
125, 10cfv 6563 . . . . 5 class (𝑐𝑛)
1311, 12, 2wbr 5148 . . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐𝑛)
1410cdm 5689 . . . . 5 class dom 𝑐
15 cc0 11153 . . . . . 6 class 0
1615csn 4631 . . . . 5 class {0}
1714, 16cdif 3960 . . . 4 class (dom 𝑐 ∖ {0})
1813, 4, 17wral 3059 . . 3 wff 𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛)
191cword 14549 . . 3 class Word 𝐴
2018, 9, 19crab 3433 . 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛)}
213, 20wceq 1537 1 wff ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛)}
Colors of variables: wff setvar class
This definition is referenced by:  ischn  32981
  Copyright terms: Public domain W3C validator