Definition df-drs 18389

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 18387	. 2 class Dirset
2		vb	. . . . . . . 8 setvar 𝑏
3	2	cv 1569	. . . . . . 7 class 𝑏
4		c0 4282	. . . . . . 7 class ∅
5	3, 4	wne 2957	. . . . . 6 wff 𝑏 ≠ ∅
6		vx	. . . . . . . . . . . 12 setvar 𝑥
7	6	cv 1569	. . . . . . . . . . 11 class 𝑥
8		vz	. . . . . . . . . . . 12 setvar 𝑧
9	8	cv 1569	. . . . . . . . . . 11 class 𝑧
10		vr	. . . . . . . . . . . 12 setvar 𝑟
11	10	cv 1569	. . . . . . . . . . 11 class 𝑟
12	7, 9, 11	wbr 5107	. . . . . . . . . 10 wff 𝑥𝑟𝑧
13		vy	. . . . . . . . . . . 12 setvar 𝑦
14	13	cv 1569	. . . . . . . . . . 11 class 𝑦
15	14, 9, 11	wbr 5107	. . . . . . . . . 10 wff 𝑦𝑟𝑧
16	12, 15	wa 401	. . . . . . . . 9 wff (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
17	16, 8, 3	wrex 3088	. . . . . . . 8 wff ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
18	17, 13, 3	wral 3078	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
19	18, 6, 3	wral 3078	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)
20	5, 19	wa 401	. . . . 5 wff (𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
21		vf	. . . . . . 7 setvar 𝑓
22	21	cv 1569	. . . . . 6 class 𝑓
23		cple 17355	. . . . . 6 class le
24	22, 23	cfv 6537	. . . . 5 class (le‘𝑓)
25	20, 10, 24	wsbc 3742	. . . 4 wff [(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
26		cbs 17307	. . . . 5 class Base
27	22, 26	cfv 6537	. . . 4 class (Base‘𝑓)
28	25, 2, 27	wsbc 3742	. . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))
29		cproset 18386	. . 3 class Proset
30	28, 21, 29	crab 3414	. 2 class {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}
31	1, 30	wceq 1570	1 wff Dirset = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}

This definition is used by:  isdrs  18395