MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-preset Structured version   Unicode version

Definition df-preset 14390
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.)

Assertion
Ref Expression
df-preset  |-  Preset  =  {
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 ) ) }
Distinct variable group:    f, b, r, x, y, z

Detailed syntax breakdown of Definition df-preset
StepHypRef Expression
1 cpreset 14388 . 2  class  Preset
2 vx . . . . . . . . . . 11  set  x
32cv 1652 . . . . . . . . . 10  class  x
4 vr . . . . . . . . . . 11  set  r
54cv 1652 . . . . . . . . . 10  class  r
63, 3, 5wbr 4215 . . . . . . . . 9  wff  x r x
7 vy . . . . . . . . . . . . 13  set  y
87cv 1652 . . . . . . . . . . . 12  class  y
93, 8, 5wbr 4215 . . . . . . . . . . 11  wff  x r y
10 vz . . . . . . . . . . . . 13  set  z
1110cv 1652 . . . . . . . . . . . 12  class  z
128, 11, 5wbr 4215 . . . . . . . . . . 11  wff  y r z
139, 12wa 360 . . . . . . . . . 10  wff  ( x r y  /\  y
r z )
143, 11, 5wbr 4215 . . . . . . . . . 10  wff  x r z
1513, 14wi 4 . . . . . . . . 9  wff  ( ( x r y  /\  y r z )  ->  x r z )
166, 15wa 360 . . . . . . . 8  wff  ( x r x  /\  (
( x r y  /\  y r z )  ->  x r
z ) )
17 vb . . . . . . . . 9  set  b
1817cv 1652 . . . . . . . 8  class  b
1916, 10, 18wral 2707 . . . . . . 7  wff  A. z  e.  b  ( x
r x  /\  (
( x r y  /\  y r z )  ->  x r
z ) )
2019, 7, 18wral 2707 . . . . . 6  wff  A. y  e.  b  A. z  e.  b  ( x
r x  /\  (
( x r y  /\  y r z )  ->  x r
z ) )
2120, 2, 18wral 2707 . . . . 5  wff  A. x  e.  b  A. y  e.  b  A. z  e.  b  ( x
r x  /\  (
( x r y  /\  y r z )  ->  x r
z ) )
22 vf . . . . . . 7  set  f
2322cv 1652 . . . . . 6  class  f
24 cple 13541 . . . . . 6  class  le
2523, 24cfv 5457 . . . . 5  class  ( le
`  f )
2621, 4, 25wsbc 3163 . . . 4  wff  [. ( 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 ) )
27 cbs 13474 . . . . 5  class  Base
2823, 27cfv 5457 . . . 4  class  ( Base `  f )
2926, 17, 28wsbc 3163 . . 3  wff  [. ( 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 ) )
3029, 22cab 2424 . 2  class  { 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 ) ) }
311, 30wceq 1653 1  wff  Preset  =  {
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 ) ) }
Colors of variables: wff set class
This definition is referenced by:  isprs  14392
  Copyright terms: Public domain W3C validator