Description: Define the class of preordered sets, or prosets. A proset is a set equipped with a preorder, that is, a transitive and reflexive relation.
Preorders are a natural generalization of partial orders which need not be antisymmetric: there may be pairs of elements such that each is "less than or equal to" the other, so that both elements have the same order-theoretic properties (in some sense, there is a "tie" among them).
If a preorder is required to be antisymmetric, that is, there is no such "tie", then one obtains a partial order. If a preorder is required to be symmetric, that is, all comparable elements are tied, then one obtains an equivalence relation.
Every preorder naturally factors into these two notions: the "tie" relation on a proset is an equivalence relation, and the quotient under that equivalence relation is a partial order. (Contributed by FL, 17-Nov-2014) (Revised by Stefan O'Rear, 31-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-proset | |- Proset = { f | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cproset | |- Proset |
|
1 | vf | |- f |
|
2 | cbs | |- Base |
|
3 | 1 | cv | |- f |
4 | 3 2 | cfv | |- ( Base ` f ) |
5 | vb | |- b |
|
6 | cple | |- le |
|
7 | 3 6 | cfv | |- ( le ` f ) |
8 | vr | |- r |
|
9 | vx | |- x |
|
10 | 5 | cv | |- b |
11 | vy | |- y |
|
12 | vz | |- z |
|
13 | 9 | cv | |- x |
14 | 8 | cv | |- r |
15 | 13 13 14 | wbr | |- x r x |
16 | 11 | cv | |- y |
17 | 13 16 14 | wbr | |- x r y |
18 | 12 | cv | |- z |
19 | 16 18 14 | wbr | |- y r z |
20 | 17 19 | wa | |- ( x r y /\ y r z ) |
21 | 13 18 14 | wbr | |- x r z |
22 | 20 21 | wi | |- ( ( x r y /\ y r z ) -> x r z ) |
23 | 15 22 | wa | |- ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) |
24 | 23 12 10 | wral | |- A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) |
25 | 24 11 10 | wral | |- A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) |
26 | 25 9 10 | wral | |- A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) |
27 | 26 8 7 | wsbc | |- [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) |
28 | 27 5 4 | wsbc | |- [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) |
29 | 28 1 | cab | |- { f | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) } |
30 | 0 29 | wceq | |- Proset = { f | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) } |