Definition df-proset 18022

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

Step	Hyp	Ref	Expression
1		cproset 18020	. 2 class Proset
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1538	. . . . . . . . . 10 class 𝑥
4		vr	. . . . . . . . . . 11 setvar 𝑟
5	4	cv 1538	. . . . . . . . . 10 class 𝑟
6	3, 3, 5	wbr 5075	. . . . . . . . 9 wff 𝑥𝑟𝑥
7		vy	. . . . . . . . . . . . 13 setvar 𝑦
8	7	cv 1538	. . . . . . . . . . . 12 class 𝑦
9	3, 8, 5	wbr 5075	. . . . . . . . . . 11 wff 𝑥𝑟𝑦
10		vz	. . . . . . . . . . . . 13 setvar 𝑧
11	10	cv 1538	. . . . . . . . . . . 12 class 𝑧
12	8, 11, 5	wbr 5075	. . . . . . . . . . 11 wff 𝑦𝑟𝑧
13	9, 12	wa 396	. . . . . . . . . 10 wff (𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧)
14	3, 11, 5	wbr 5075	. . . . . . . . . 10 wff 𝑥𝑟𝑧
15	13, 14	wi 4	. . . . . . . . 9 wff ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)
16	6, 15	wa 396	. . . . . . . 8 wff (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
17		vb	. . . . . . . . 9 setvar 𝑏
18	17	cv 1538	. . . . . . . 8 class 𝑏
19	16, 10, 18	wral 3065	. . . . . . 7 wff ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
20	19, 7, 18	wral 3065	. . . . . 6 wff ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
21	20, 2, 18	wral 3065	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
22		vf	. . . . . . 7 setvar 𝑓
23	22	cv 1538	. . . . . 6 class 𝑓
24		cple 16978	. . . . . 6 class le
25	23, 24	cfv 6437	. . . . 5 class (le‘𝑓)
26	21, 4, 25	wsbc 3717	. . . 4 wff [(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
27		cbs 16921	. . . . 5 class Base
28	23, 27	cfv 6437	. . . 4 class (Base‘𝑓)
29	26, 17, 28	wsbc 3717	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
30	29, 22	cab 2716	. 2 class {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
31	1, 30	wceq 1539	1 wff Proset = {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}

This definition is referenced by:  isprs  18024