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 32996
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 32995 . 2 class ( < Chain𝐴)
4 vn . . . . . . . 8 setvar 𝑛
54cv 1538 . . . . . . 7 class 𝑛
6 c1 11157 . . . . . . 7 class 1
7 cmin 11493 . . . . . . 7 class
85, 6, 7co 7432 . . . . . 6 class (𝑛 − 1)
9 vc . . . . . . 7 setvar 𝑐
109cv 1538 . . . . . 6 class 𝑐
118, 10cfv 6560 . . . . 5 class (𝑐‘(𝑛 − 1))
125, 10cfv 6560 . . . . 5 class (𝑐𝑛)
1311, 12, 2wbr 5142 . . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐𝑛)
1410cdm 5684 . . . . 5 class dom 𝑐
15 cc0 11156 . . . . . 6 class 0
1615csn 4625 . . . . 5 class {0}
1714, 16cdif 3947 . . . 4 class (dom 𝑐 ∖ {0})
1813, 4, 17wral 3060 . . 3 wff 𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛)
191cword 14553 . . 3 class Word 𝐴
2018, 9, 19crab 3435 . 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛)}
213, 20wceq 1539 1 wff ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛)}
Colors of variables: wff setvar class
This definition is referenced by:  ischn  32997
  Copyright terms: Public domain W3C validator