Definition df-drs 17137

Description: Define the class of directed sets. A directed set is a nonempty preordered set where every pair of elements have some upper bound. Note that it is not required that there exist a least upper bound.

There is no consensus in the literature over whether directed sets are allowed to be empty. It is slightly more convenient for us if they are not. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Assertion

Ref	Expression
df-drs	⊢ Dirset = {𝑓 ∈ Preset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}

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

Detailed syntax breakdown of Definition df-drs

Step	Hyp	Ref	Expression
1		cdrs 17135	. 2 class Dirset
2		vb	. . . . . . . 8 setvar 𝑏
3	2	cv 1630	. . . . . . 7 class 𝑏
4		c0 4063	. . . . . . 7 class ∅
5	3, 4	wne 2943	. . . . . 6 wff 𝑏 ≠ ∅
6		vx	. . . . . . . . . . . 12 setvar 𝑥
7	6	cv 1630	. . . . . . . . . . 11 class 𝑥
8		vz	. . . . . . . . . . . 12 setvar 𝑧
9	8	cv 1630	. . . . . . . . . . 11 class 𝑧
10		vr	. . . . . . . . . . . 12 setvar 𝑟
11	10	cv 1630	. . . . . . . . . . 11 class 𝑟
12	7, 9, 11	wbr 4786	. . . . . . . . . 10 wff 𝑥𝑟𝑧
13		vy	. . . . . . . . . . . 12 setvar 𝑦
14	13	cv 1630	. . . . . . . . . . 11 class 𝑦
15	14, 9, 11	wbr 4786	. . . . . . . . . 10 wff 𝑦𝑟𝑧
16	12, 15	wa 382	. . . . . . . . 9 wff (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
17	16, 8, 3	wrex 3062	. . . . . . . 8 wff ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
18	17, 13, 3	wral 3061	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
19	18, 6, 3	wral 3061	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
20	5, 19	wa 382	. . . . 5 wff (𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
21		vf	. . . . . . 7 setvar 𝑓
22	21	cv 1630	. . . . . 6 class 𝑓
23		cple 16156	. . . . . 6 class le
24	22, 23	cfv 6031	. . . . 5 class (le‘𝑓)
25	20, 10, 24	wsbc 3587	. . . 4 wff [(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
26		cbs 16064	. . . . 5 class Base
27	22, 26	cfv 6031	. . . 4 class (Base‘𝑓)
28	25, 2, 27	wsbc 3587	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
29		cpreset 17134	. . 3 class Preset
30	28, 21, 29	crab 3065	. 2 class {𝑓 ∈ Preset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}
31	1, 30	wceq 1631	1 wff Dirset = {𝑓 ∈ Preset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}

This definition is referenced by:  isdrs  17142