Definition df-preset 16928

Description: Define the class of preordered sets (presets). A preset is a set equipped with a transitive and reflexive relation.

Preorders are a natural generalization of order for sets where there is a well-defined ordering, but it in some sense "fails to capture the whole story", in that there may be pairs of elements which are indistinguishable under the order. Two elements which are not equal but are less-or-equal to each other behave the same under all order operations and may be thought of as "tied".

A preorder can naturally be strengthened by requiring that there are no ties, resulting in a partial order, or by stating that all comparable pairs of elements are tied, resulting in an equivalence relation. Every preorder naturally factors into these two types; the tied relation on a preorder is an equivalence relation and the quotient under that relation is a partial order. (Contributed by FL, 17-Nov-2014.) (Revised by Stefan O'Rear, 31-Jan-2015.)

Assertion

Ref	Expression
df-preset	⊢ Preset = {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}

Distinct variable group:   𝑓,𝑏,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-preset

Step	Hyp	Ref	Expression
1		cpreset 16926	. 2 class Preset
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1482	. . . . . . . . . 10 class 𝑥
4		vr	. . . . . . . . . . 11 setvar 𝑟
5	4	cv 1482	. . . . . . . . . 10 class 𝑟
6	3, 3, 5	wbr 4653	. . . . . . . . 9 wff 𝑥𝑟𝑥
7		vy	. . . . . . . . . . . . 13 setvar 𝑦
8	7	cv 1482	. . . . . . . . . . . 12 class 𝑦
9	3, 8, 5	wbr 4653	. . . . . . . . . . 11 wff 𝑥𝑟𝑦
10		vz	. . . . . . . . . . . . 13 setvar 𝑧
11	10	cv 1482	. . . . . . . . . . . 12 class 𝑧
12	8, 11, 5	wbr 4653	. . . . . . . . . . 11 wff 𝑦𝑟𝑧
13	9, 12	wa 384	. . . . . . . . . 10 wff (𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧)
14	3, 11, 5	wbr 4653	. . . . . . . . . 10 wff 𝑥𝑟𝑧
15	13, 14	wi 4	. . . . . . . . 9 wff ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)
16	6, 15	wa 384	. . . . . . . 8 wff (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
17		vb	. . . . . . . . 9 setvar 𝑏
18	17	cv 1482	. . . . . . . 8 class 𝑏
19	16, 10, 18	wral 2912	. . . . . . 7 wff ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
20	19, 7, 18	wral 2912	. . . . . 6 wff ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
21	20, 2, 18	wral 2912	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
22		vf	. . . . . . 7 setvar 𝑓
23	22	cv 1482	. . . . . 6 class 𝑓
24		cple 15948	. . . . . 6 class le
25	23, 24	cfv 5888	. . . . 5 class (le‘𝑓)
26	21, 4, 25	wsbc 3435	. . . 4 wff [(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
27		cbs 15857	. . . . 5 class Base
28	23, 27	cfv 5888	. . . 4 class (Base‘𝑓)
29	26, 17, 28	wsbc 3435	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))
30	29, 22	cab 2608	. 2 class {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
31	1, 30	wceq 1483	1 wff Preset = {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}

This definition is referenced by:  isprs  16930