Definition df-drs 17539

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 17537	. 2 class Dirset
2		vb	. . . . . . . 8 setvar 𝑏
3	2	cv 1536	. . . . . . 7 class 𝑏
4		c0 4291	. . . . . . 7 class ∅
5	3, 4	wne 3016	. . . . . 6 wff 𝑏 ≠ ∅
6		vx	. . . . . . . . . . . 12 setvar 𝑥
7	6	cv 1536	. . . . . . . . . . 11 class 𝑥
8		vz	. . . . . . . . . . . 12 setvar 𝑧
9	8	cv 1536	. . . . . . . . . . 11 class 𝑧
10		vr	. . . . . . . . . . . 12 setvar 𝑟
11	10	cv 1536	. . . . . . . . . . 11 class 𝑟
12	7, 9, 11	wbr 5066	. . . . . . . . . 10 wff 𝑥𝑟𝑧
13		vy	. . . . . . . . . . . 12 setvar 𝑦
14	13	cv 1536	. . . . . . . . . . 11 class 𝑦
15	14, 9, 11	wbr 5066	. . . . . . . . . 10 wff 𝑦𝑟𝑧
16	12, 15	wa 398	. . . . . . . . 9 wff (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
17	16, 8, 3	wrex 3139	. . . . . . . 8 wff ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
18	17, 13, 3	wral 3138	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
19	18, 6, 3	wral 3138	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
20	5, 19	wa 398	. . . . 5 wff (𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
21		vf	. . . . . . 7 setvar 𝑓
22	21	cv 1536	. . . . . 6 class 𝑓
23		cple 16572	. . . . . 6 class le
24	22, 23	cfv 6355	. . . . 5 class (le‘𝑓)
25	20, 10, 24	wsbc 3772	. . . 4 wff [(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
26		cbs 16483	. . . . 5 class Base
27	22, 26	cfv 6355	. . . 4 class (Base‘𝑓)
28	25, 2, 27	wsbc 3772	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
29		cproset 17536	. . 3 class Proset
30	28, 21, 29	crab 3142	. 2 class {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}
31	1, 30	wceq 1537	1 wff Dirset = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}

This definition is referenced by:  isdrs  17544