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 \| \underset{˙}{[} {Base}_{f} / b \underset{˙}{]} \underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to 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 \leq_{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 \land y r z)$
21	13 18 14	wbr	$wff x r z$
22	20 21	wi	$wff ((x r y \land y r z) \to x r z)$
23	15 22	wa	$wff (x r x \land ((x r y \land y r z) \to x r z))$
24	23 12 10	wral	$wff \forall z \in b (x r x \land ((x r y \land y r z) \to x r z))$
25	24 11 10	wral	$wff \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z))$
26	25 9 10	wral	$wff \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z))$
27	26 8 7	wsbc	$wff \underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z))$
28	27 5 4	wsbc	$wff \underset{˙}{[} {Base}_{f} / b \underset{˙}{]} \underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z))$
29	28 1	cab	$class \{f \| \underset{˙}{[} {Base}_{f} / b \underset{˙}{]} \underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z))\}$
30	0 29	wceq	$wff Proset = \{f \| \underset{˙}{[} {Base}_{f} / b \underset{˙}{]} \underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z))\}$

Metamath Proof Explorer

Definition df-proset

Detailed syntax breakdown