Metamath Proof Explorer


Definition df-proset

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 ) ) }

Detailed syntax breakdown

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 ) ) }