Definition df-drs 17397

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 = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}

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

Detailed syntax breakdown of Definition df-drs

Step	Hyp	Ref	Expression
1		cdrs 17395	. 2 class Dirset
2		vb	. . . . . . . 8 setvar 𝑏
3	2	cv 1506	. . . . . . 7 class 𝑏
4		c0 4179	. . . . . . 7 class ∅
5	3, 4	wne 2968	. . . . . 6 wff 𝑏 ≠ ∅
6		vx	. . . . . . . . . . . 12 setvar 𝑥
7	6	cv 1506	. . . . . . . . . . 11 class 𝑥
8		vz	. . . . . . . . . . . 12 setvar 𝑧
9	8	cv 1506	. . . . . . . . . . 11 class 𝑧
10		vr	. . . . . . . . . . . 12 setvar 𝑟
11	10	cv 1506	. . . . . . . . . . 11 class 𝑟
12	7, 9, 11	wbr 4929	. . . . . . . . . 10 wff 𝑥𝑟𝑧
13		vy	. . . . . . . . . . . 12 setvar 𝑦
14	13	cv 1506	. . . . . . . . . . 11 class 𝑦
15	14, 9, 11	wbr 4929	. . . . . . . . . 10 wff 𝑦𝑟𝑧
16	12, 15	wa 387	. . . . . . . . 9 wff (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
17	16, 8, 3	wrex 3090	. . . . . . . 8 wff ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
18	17, 13, 3	wral 3089	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
19	18, 6, 3	wral 3089	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
20	5, 19	wa 387	. . . . 5 wff (𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
21		vf	. . . . . . 7 setvar 𝑓
22	21	cv 1506	. . . . . 6 class 𝑓
23		cple 16428	. . . . . 6 class le
24	22, 23	cfv 6188	. . . . 5 class (le‘𝑓)
25	20, 10, 24	wsbc 3682	. . . 4 wff [(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
26		cbs 16339	. . . . 5 class Base
27	22, 26	cfv 6188	. . . 4 class (Base‘𝑓)
28	25, 2, 27	wsbc 3682	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
29		cproset 17394	. . 3 class Proset
30	28, 21, 29	crab 3093	. 2 class {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}
31	1, 30	wceq 1507	1 wff Dirset = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}

This definition is referenced by:  isdrs  17402