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]˙ [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r z → x r z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cproset class Proset
1 vf setvar f
2 cbs class Base
3 1 cv setvar f
4 3 2 cfv class Base f
5 vb setvar b
6 cple class le
7 3 6 cfv class ≤ 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 x r y ∧ y r z
21 13 18 14 wbr wff x r z
22 20 21 wi wff x r y ∧ y r z → x r z
23 15 22 wa wff x r x ∧ x r y ∧ y r z → x r z
24 23 12 10 wral wff ∀ z ∈ b x r x ∧ x r y ∧ y r z → x r z
25 24 11 10 wral wff ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r z → x r z
26 25 9 10 wral wff ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r z → x r z
27 26 8 7 wsbc wff [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r z → x r z
28 27 5 4 wsbc wff [˙Base f / b]˙ [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r z → x r z
29 28 1 cab class f | [˙Base f / b]˙ [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r z → x r z
30 0 29 wceq wff Proset = f | [˙Base f / b]˙ [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x r x ∧ x r y ∧ y r z → x r z