Definition df-drs 18230

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 18228	. 2 class Dirset
2		vb	. . . . . . . 8 setvar 𝑏
3	2	cv 1541	. . . . . . 7 class 𝑏
4		c0 4287	. . . . . . 7 class ∅
5	3, 4	wne 2933	. . . . . 6 wff 𝑏 ≠ ∅
6		vx	. . . . . . . . . . . 12 setvar 𝑥
7	6	cv 1541	. . . . . . . . . . 11 class 𝑥
8		vz	. . . . . . . . . . . 12 setvar 𝑧
9	8	cv 1541	. . . . . . . . . . 11 class 𝑧
10		vr	. . . . . . . . . . . 12 setvar 𝑟
11	10	cv 1541	. . . . . . . . . . 11 class 𝑟
12	7, 9, 11	wbr 5100	. . . . . . . . . 10 wff 𝑥𝑟𝑧
13		vy	. . . . . . . . . . . 12 setvar 𝑦
14	13	cv 1541	. . . . . . . . . . 11 class 𝑦
15	14, 9, 11	wbr 5100	. . . . . . . . . 10 wff 𝑦𝑟𝑧
16	12, 15	wa 395	. . . . . . . . 9 wff (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
17	16, 8, 3	wrex 3062	. . . . . . . 8 wff ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
18	17, 13, 3	wral 3052	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
19	18, 6, 3	wral 3052	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
20	5, 19	wa 395	. . . . 5 wff (𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
21		vf	. . . . . . 7 setvar 𝑓
22	21	cv 1541	. . . . . 6 class 𝑓
23		cple 17196	. . . . . 6 class le
24	22, 23	cfv 6500	. . . . 5 class (le‘𝑓)
25	20, 10, 24	wsbc 3742	. . . 4 wff [(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
26		cbs 17148	. . . . 5 class Base
27	22, 26	cfv 6500	. . . 4 class (Base‘𝑓)
28	25, 2, 27	wsbc 3742	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
29		cproset 18227	. . 3 class Proset
30	28, 21, 29	crab 3401	. 2 class {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}
31	1, 30	wceq 1542	1 wff Dirset = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}

This definition is referenced by:  isdrs  18236