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

Definition df-drs 14378
 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 14376 . 2 Dirset
2 vb . . . . . . . 8
32cv 1651 . . . . . . 7
4 c0 3620 . . . . . . 7
53, 4wne 2598 . . . . . 6
6 vx . . . . . . . . . . . 12
76cv 1651 . . . . . . . . . . 11
8 vz . . . . . . . . . . . 12
98cv 1651 . . . . . . . . . . 11
10 vr . . . . . . . . . . . 12
1110cv 1651 . . . . . . . . . . 11
127, 9, 11wbr 4204 . . . . . . . . . 10
13 vy . . . . . . . . . . . 12
1413cv 1651 . . . . . . . . . . 11
1514, 9, 11wbr 4204 . . . . . . . . . 10
1612, 15wa 359 . . . . . . . . 9
1716, 8, 3wrex 2698 . . . . . . . 8
1817, 13, 3wral 2697 . . . . . . 7
1918, 6, 3wral 2697 . . . . . 6
205, 19wa 359 . . . . 5
21 vf . . . . . . 7
2221cv 1651 . . . . . 6
23 cple 13528 . . . . . 6
2422, 23cfv 5446 . . . . 5
2520, 10, 24wsbc 3153 . . . 4
26 cbs 13461 . . . . 5
2722, 26cfv 5446 . . . 4
2825, 2, 27wsbc 3153 . . 3
29 cpreset 14375 . . 3
3028, 21, 29crab 2701 . 2
311, 30wceq 1652 1 Dirset
 Colors of variables: wff set class This definition is referenced by:  isdrs  14383
 Copyright terms: Public domain W3C validator