![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-preset | Structured version Visualization version Unicode version |
Description: Define the class of
preordered sets (presets). A preset is a set
equipped with a transitive and reflexive relation.
Preorders are a natural generalization of order for sets where there is a well-defined ordering, but it in some sense "fails to capture the whole story", in that there may be pairs of elements which are indistinguishable under the order. Two elements which are not equal but are less-or-equal to each other behave the same under all order operations and may be thought of as "tied". A preorder can naturally be strengthened by requiring that there are no ties, resulting in a partial order, or by stating that all comparable pairs of elements are tied, resulting in an equivalence relation. Every preorder naturally factors into these two types; the tied relation on a preorder is an equivalence relation and the quotient under that relation is a partial order. (Contributed by FL, 17-Nov-2014.) (Revised by Stefan O'Rear, 31-Jan-2015.) |
Ref | Expression |
---|---|
df-preset |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpreset 16171 |
. 2
![]() ![]() | |
2 | vx |
. . . . . . . . . . 11
![]() ![]() | |
3 | 2 | cv 1443 |
. . . . . . . . . 10
![]() ![]() |
4 | vr |
. . . . . . . . . . 11
![]() ![]() | |
5 | 4 | cv 1443 |
. . . . . . . . . 10
![]() ![]() |
6 | 3, 3, 5 | wbr 4402 |
. . . . . . . . 9
![]() ![]() ![]() ![]() |
7 | vy |
. . . . . . . . . . . . 13
![]() ![]() | |
8 | 7 | cv 1443 |
. . . . . . . . . . . 12
![]() ![]() |
9 | 3, 8, 5 | wbr 4402 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() |
10 | vz |
. . . . . . . . . . . . 13
![]() ![]() | |
11 | 10 | cv 1443 |
. . . . . . . . . . . 12
![]() ![]() |
12 | 8, 11, 5 | wbr 4402 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() |
13 | 9, 12 | wa 371 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 3, 11, 5 | wbr 4402 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() |
15 | 13, 14 | wi 4 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 6, 15 | wa 371 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | vb |
. . . . . . . . 9
![]() ![]() | |
18 | 17 | cv 1443 |
. . . . . . . 8
![]() ![]() |
19 | 16, 10, 18 | wral 2737 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 19, 7, 18 | wral 2737 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 20, 2, 18 | wral 2737 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | vf |
. . . . . . 7
![]() ![]() | |
23 | 22 | cv 1443 |
. . . . . 6
![]() ![]() |
24 | cple 15197 |
. . . . . 6
![]() ![]() | |
25 | 23, 24 | cfv 5582 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
26 | 21, 4, 25 | wsbc 3267 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
27 | cbs 15121 |
. . . . 5
![]() ![]() | |
28 | 23, 27 | cfv 5582 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
29 | 26, 17, 28 | wsbc 3267 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | 29, 22 | cab 2437 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 1, 30 | wceq 1444 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: isprs 16175 |
Copyright terms: Public domain | W3C validator |