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 ]. [. ( 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 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cproset	|- Proset
1		vf	|- f
2		cbs	|- Base
3	1	cv	|- f
4	3 2	cfv	|- ( Base ` f )
5		vb	|- b
6		cple	|- le
7	3 6	cfv	|- ( le ` f )
8		vr	|- r
9		vx	|- x
10	5	cv	|- b
11		vy	|- y
12		vz	|- z
13	9	cv	|- x
14	8	cv	|- r
15	13 13 14	wbr	|- x r x
16	11	cv	|- y
17	13 16 14	wbr	|- x r y
18	12	cv	|- z
19	16 18 14	wbr	|- y r z
20	17 19	wa	|- ( x r y /\ y r z )
21	13 18 14	wbr	|- x r z
22	20 21	wi	|- ( ( x r y /\ y r z ) -> x r z )
23	15 22	wa	|- ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) )
24	23 12 10	wral	|- A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) )
25	24 11 10	wral	|- A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) )
26	25 9 10	wral	|- 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	26 8 7	wsbc	|- [. ( 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 ) )
28	27 5 4	wsbc	|- [. ( 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 ) )
29	28 1	cab	|- { 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 ) ) }
30	0 29	wceq	|- Proset = { 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 ) ) }