Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-drs Structured version   Unicode version

Definition df-drs 16125
 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
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-drs
StepHypRef Expression
1 cdrs 16123 . 2 Dirset
2 vb . . . . . . . 8
32cv 1436 . . . . . . 7
4 c0 3767 . . . . . . 7
53, 4wne 2625 . . . . . 6
6 vx . . . . . . . . . . . 12
76cv 1436 . . . . . . . . . . 11
8 vz . . . . . . . . . . . 12
98cv 1436 . . . . . . . . . . 11
10 vr . . . . . . . . . . . 12
1110cv 1436 . . . . . . . . . . 11
127, 9, 11wbr 4426 . . . . . . . . . 10
13 vy . . . . . . . . . . . 12
1413cv 1436 . . . . . . . . . . 11
1514, 9, 11wbr 4426 . . . . . . . . . 10
1612, 15wa 370 . . . . . . . . 9
1716, 8, 3wrex 2783 . . . . . . . 8
1817, 13, 3wral 2782 . . . . . . 7
1918, 6, 3wral 2782 . . . . . 6
205, 19wa 370 . . . . 5
21 vf . . . . . . 7
2221cv 1436 . . . . . 6
23 cple 15159 . . . . . 6
2422, 23cfv 5601 . . . . 5
2520, 10, 24wsbc 3305 . . . 4
26 cbs 15084 . . . . 5
2722, 26cfv 5601 . . . 4
2825, 2, 27wsbc 3305 . . 3
29 cpreset 16122 . . 3
3028, 21, 29crab 2786 . 2
311, 30wceq 1437 1 Dirset
 Colors of variables: wff setvar class This definition is referenced by:  isdrs  16130
 Copyright terms: Public domain W3C validator