# 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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cproset ${class}\mathrm{Proset}$
1 vf ${setvar}{f}$
2 cbs ${class}\mathrm{Base}$
3 1 cv ${setvar}{f}$
4 3 2 cfv ${class}{\mathrm{Base}}_{{f}}$
5 vb ${setvar}{b}$
6 cple ${class}\mathrm{le}$
7 3 6 cfv ${class}{\le }_{{f}}$
8 vr ${setvar}{r}$
9 vx ${setvar}{x}$
10 5 cv ${setvar}{b}$
11 vy ${setvar}{y}$
12 vz ${setvar}{z}$
13 9 cv ${setvar}{x}$
14 8 cv ${setvar}{r}$
15 13 13 14 wbr ${wff}{x}{r}{x}$
16 11 cv ${setvar}{y}$
17 13 16 14 wbr ${wff}{x}{r}{y}$
18 12 cv ${setvar}{z}$
19 16 18 14 wbr ${wff}{y}{r}{z}$
20 17 19 wa ${wff}\left({x}{r}{y}\wedge {y}{r}{z}\right)$
21 13 18 14 wbr ${wff}{x}{r}{z}$
22 20 21 wi ${wff}\left(\left({x}{r}{y}\wedge {y}{r}{z}\right)\to {x}{r}{z}\right)$
23 15 22 wa ${wff}\left({x}{r}{x}\wedge \left(\left({x}{r}{y}\wedge {y}{r}{z}\right)\to {x}{r}{z}\right)\right)$
24 23 12 10 wral ${wff}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}\left({x}{r}{x}\wedge \left(\left({x}{r}{y}\wedge {y}{r}{z}\right)\to {x}{r}{z}\right)\right)$
25 24 11 10 wral ${wff}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}\left({x}{r}{x}\wedge \left(\left({x}{r}{y}\wedge {y}{r}{z}\right)\to {x}{r}{z}\right)\right)$
26 25 9 10 wral ${wff}\forall {x}\in {b}\phantom{\rule{.4em}{0ex}}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}\left({x}{r}{x}\wedge \left(\left({x}{r}{y}\wedge {y}{r}{z}\right)\to {x}{r}{z}\right)\right)$
27 26 8 7 wsbc
28 27 5 4 wsbc
29 28 1 cab
30 0 29 wceq