Definition df-drs 16929

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 = { f e. Preset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) }

Distinct variable group:   f, b, r, x, y, z

Detailed syntax breakdown of Definition df-drs

Step	Hyp	Ref	Expression
1		cdrs 16927	. 2 class Dirset
2		vb	. . . . . . . 8 setvar b
3	2	cv 1482	. . . . . . 7 class b
4		c0 3915	. . . . . . 7 class (/)
5	3, 4	wne 2794	. . . . . 6 wff b =/= (/)
6		vx	. . . . . . . . . . . 12 setvar x
7	6	cv 1482	. . . . . . . . . . 11 class x
8		vz	. . . . . . . . . . . 12 setvar z
9	8	cv 1482	. . . . . . . . . . 11 class z
10		vr	. . . . . . . . . . . 12 setvar r
11	10	cv 1482	. . . . . . . . . . 11 class r
12	7, 9, 11	wbr 4653	. . . . . . . . . 10 wff x r z
13		vy	. . . . . . . . . . . 12 setvar y
14	13	cv 1482	. . . . . . . . . . 11 class y
15	14, 9, 11	wbr 4653	. . . . . . . . . 10 wff y r z
16	12, 15	wa 384	. . . . . . . . 9 wff ( x r z /\ y r z )
17	16, 8, 3	wrex 2913	. . . . . . . 8 wff E. z e. b ( x r z /\ y r z )
18	17, 13, 3	wral 2912	. . . . . . 7 wff A. y e. b E. z e. b ( x r z /\ y r z )
19	18, 6, 3	wral 2912	. . . . . 6 wff A. x e. b A. y e. b E. z e. b ( x r z /\ y r z )
20	5, 19	wa 384	. . . . 5 wff ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) )
21		vf	. . . . . . 7 setvar f
22	21	cv 1482	. . . . . 6 class f
23		cple 15948	. . . . . 6 class le
24	22, 23	cfv 5888	. . . . 5 class ( le ` f )
25	20, 10, 24	wsbc 3435	. . . 4 wff [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) )
26		cbs 15857	. . . . 5 class Base
27	22, 26	cfv 5888	. . . 4 class ( Base ` f )
28	25, 2, 27	wsbc 3435	. . 3 wff [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) )
29		cpreset 16926	. . 3 class Preset
30	28, 21, 29	crab 2916	. 2 class { f e. Preset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) }
31	1, 30	wceq 1483	1 wff Dirset = { f e. Preset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) }

This definition is referenced by:  isdrs  16934