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

Definition df-proset 17617
 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.)
Assertion
Ref Expression
df-proset Proset = {𝑓[(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
Distinct variable group:   𝑓,𝑏,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-proset
StepHypRef Expression
1 cproset 17615 . 2 class Proset
2 vx . . . . . . . . . . 11 setvar 𝑥
32cv 1537 . . . . . . . . . 10 class 𝑥
4 vr . . . . . . . . . . 11 setvar 𝑟
54cv 1537 . . . . . . . . . 10 class 𝑟
63, 3, 5wbr 5036 . . . . . . . . 9 wff 𝑥𝑟𝑥
7 vy . . . . . . . . . . . . 13 setvar 𝑦
87cv 1537 . . . . . . . . . . . 12 class 𝑦
93, 8, 5wbr 5036 . . . . . . . . . . 11 wff 𝑥𝑟𝑦
10 vz . . . . . . . . . . . . 13 setvar 𝑧
1110cv 1537 . . . . . . . . . . . 12 class 𝑧
128, 11, 5wbr 5036 . . . . . . . . . . 11 wff 𝑦𝑟𝑧
139, 12wa 399 . . . . . . . . . 10 wff (𝑥𝑟𝑦𝑦𝑟𝑧)
143, 11, 5wbr 5036 . . . . . . . . . 10 wff 𝑥𝑟𝑧
1513, 14wi 4 . . . . . . . . 9 wff ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧)
166, 15wa 399 . . . . . . . 8 wff (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
17 vb . . . . . . . . 9 setvar 𝑏
1817cv 1537 . . . . . . . 8 class 𝑏
1916, 10, 18wral 3070 . . . . . . 7 wff 𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
2019, 7, 18wral 3070 . . . . . 6 wff 𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
2120, 2, 18wral 3070 . . . . 5 wff 𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
22 vf . . . . . . 7 setvar 𝑓
2322cv 1537 . . . . . 6 class 𝑓
24 cple 16643 . . . . . 6 class le
2523, 24cfv 6340 . . . . 5 class (le‘𝑓)
2621, 4, 25wsbc 3698 . . . 4 wff [(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
27 cbs 16554 . . . . 5 class Base
2823, 27cfv 6340 . . . 4 class (Base‘𝑓)
2926, 17, 28wsbc 3698 . . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))
3029, 22cab 2735 . 2 class {𝑓[(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
311, 30wceq 1538 1 wff Proset = {𝑓[(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
 Colors of variables: wff setvar class This definition is referenced by:  isprs  17619
 Copyright terms: Public domain W3C validator