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

Definition df-preset 16697
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 = {𝑓[(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
Distinct variable group:   𝑓,𝑏,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-preset
StepHypRef Expression
1 cpreset 16695 . 2 class Preset
2 vx . . . . . . . . . . 11 setvar 𝑥
32cv 1473 . . . . . . . . . 10 class 𝑥
4 vr . . . . . . . . . . 11 setvar 𝑟
54cv 1473 . . . . . . . . . 10 class 𝑟
63, 3, 5wbr 4577 . . . . . . . . 9 wff 𝑥𝑟𝑥
7 vy . . . . . . . . . . . . 13 setvar 𝑦
87cv 1473 . . . . . . . . . . . 12 class 𝑦
93, 8, 5wbr 4577 . . . . . . . . . . 11 wff 𝑥𝑟𝑦
10 vz . . . . . . . . . . . . 13 setvar 𝑧
1110cv 1473 . . . . . . . . . . . 12 class 𝑧
128, 11, 5wbr 4577 . . . . . . . . . . 11 wff 𝑦𝑟𝑧
139, 12wa 382 . . . . . . . . . 10 wff (𝑥𝑟𝑦𝑦𝑟𝑧)
143, 11, 5wbr 4577 . . . . . . . . . 10 wff 𝑥𝑟𝑧
1513, 14wi 4 . . . . . . . . 9 wff ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)
166, 15wa 382 . . . . . . . 8 wff (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
17 vb . . . . . . . . 9 setvar 𝑏
1817cv 1473 . . . . . . . 8 class 𝑏
1916, 10, 18wral 2895 . . . . . . 7 wff 𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
2019, 7, 18wral 2895 . . . . . 6 wff 𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
2120, 2, 18wral 2895 . . . . 5 wff 𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
22 vf . . . . . . 7 setvar 𝑓
2322cv 1473 . . . . . 6 class 𝑓
24 cple 15721 . . . . . 6 class le
2523, 24cfv 5790 . . . . 5 class (le‘𝑓)
2621, 4, 25wsbc 3401 . . . 4 wff [(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
27 cbs 15641 . . . . 5 class Base
2823, 27cfv 5790 . . . 4 class (Base‘𝑓)
2926, 17, 28wsbc 3401 . . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
3029, 22cab 2595 . 2 class {𝑓[(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
311, 30wceq 1474 1 wff Preset = {𝑓[(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  isprs  16699
  Copyright terms: Public domain W3C validator