|   | Mathbox for Thierry Arnoux | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-chn | Structured version Visualization version GIF version | ||
| 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 | 
|---|---|
| df-chn | ⊢ ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)} | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | c.lt | . . 3 class < | |
| 3 | 1, 2 | cchn 32995 | . 2 class ( < Chain𝐴) | 
| 4 | vn | . . . . . . . 8 setvar 𝑛 | |
| 5 | 4 | cv 1538 | . . . . . . 7 class 𝑛 | 
| 6 | c1 11157 | . . . . . . 7 class 1 | |
| 7 | cmin 11493 | . . . . . . 7 class − | |
| 8 | 5, 6, 7 | co 7432 | . . . . . 6 class (𝑛 − 1) | 
| 9 | vc | . . . . . . 7 setvar 𝑐 | |
| 10 | 9 | cv 1538 | . . . . . 6 class 𝑐 | 
| 11 | 8, 10 | cfv 6560 | . . . . 5 class (𝑐‘(𝑛 − 1)) | 
| 12 | 5, 10 | cfv 6560 | . . . . 5 class (𝑐‘𝑛) | 
| 13 | 11, 12, 2 | wbr 5142 | . . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛) | 
| 14 | 10 | cdm 5684 | . . . . 5 class dom 𝑐 | 
| 15 | cc0 11156 | . . . . . 6 class 0 | |
| 16 | 15 | csn 4625 | . . . . 5 class {0} | 
| 17 | 14, 16 | cdif 3947 | . . . 4 class (dom 𝑐 ∖ {0}) | 
| 18 | 13, 4, 17 | wral 3060 | . . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛) | 
| 19 | 1 | cword 14553 | . . 3 class Word 𝐴 | 
| 20 | 18, 9, 19 | crab 3435 | . 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)} | 
| 21 | 3, 20 | wceq 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 |