![]() |
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 32979 | . 2 class ( < Chain𝐴) |
4 | vn | . . . . . . . 8 setvar 𝑛 | |
5 | 4 | cv 1536 | . . . . . . 7 class 𝑛 |
6 | c1 11154 | . . . . . . 7 class 1 | |
7 | cmin 11490 | . . . . . . 7 class − | |
8 | 5, 6, 7 | co 7431 | . . . . . 6 class (𝑛 − 1) |
9 | vc | . . . . . . 7 setvar 𝑐 | |
10 | 9 | cv 1536 | . . . . . 6 class 𝑐 |
11 | 8, 10 | cfv 6563 | . . . . 5 class (𝑐‘(𝑛 − 1)) |
12 | 5, 10 | cfv 6563 | . . . . 5 class (𝑐‘𝑛) |
13 | 11, 12, 2 | wbr 5148 | . . . 4 wff (𝑐‘(𝑛 − 1)) < (𝑐‘𝑛) |
14 | 10 | cdm 5689 | . . . . 5 class dom 𝑐 |
15 | cc0 11153 | . . . . . 6 class 0 | |
16 | 15 | csn 4631 | . . . . 5 class {0} |
17 | 14, 16 | cdif 3960 | . . . 4 class (dom 𝑐 ∖ {0}) |
18 | 13, 4, 17 | wral 3059 | . . 3 wff ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛) |
19 | 1 | cword 14549 | . . 3 class Word 𝐴 |
20 | 18, 9, 19 | crab 3433 | . 2 class {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)} |
21 | 3, 20 | wceq 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 |