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

Definition df-drs 14079
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
StepHypRef Expression
1 cdrs 14077 . 2  class Dirset
2 vb . . . . . . . 8  set  b
32cv 1631 . . . . . . 7  class  b
4 c0 3468 . . . . . . 7  class  (/)
53, 4wne 2459 . . . . . 6  wff  b  =/=  (/)
6 vx . . . . . . . . . . . 12  set  x
76cv 1631 . . . . . . . . . . 11  class  x
8 vz . . . . . . . . . . . 12  set  z
98cv 1631 . . . . . . . . . . 11  class  z
10 vr . . . . . . . . . . . 12  set  r
1110cv 1631 . . . . . . . . . . 11  class  r
127, 9, 11wbr 4039 . . . . . . . . . 10  wff  x r z
13 vy . . . . . . . . . . . 12  set  y
1413cv 1631 . . . . . . . . . . 11  class  y
1514, 9, 11wbr 4039 . . . . . . . . . 10  wff  y r z
1612, 15wa 358 . . . . . . . . 9  wff  ( x r z  /\  y
r z )
1716, 8, 3wrex 2557 . . . . . . . 8  wff  E. z  e.  b  ( x
r z  /\  y
r z )
1817, 13, 3wral 2556 . . . . . . 7  wff  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z )
1918, 6, 3wral 2556 . . . . . 6  wff  A. x  e.  b  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z )
205, 19wa 358 . . . . 5  wff  ( b  =/=  (/)  /\  A. x  e.  b  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z ) )
21 vf . . . . . . 7  set  f
2221cv 1631 . . . . . 6  class  f
23 cple 13231 . . . . . 6  class  le
2422, 23cfv 5271 . . . . 5  class  ( le
`  f )
2520, 10, 24wsbc 3004 . . . 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 13164 . . . . 5  class  Base
2722, 26cfv 5271 . . . 4  class  ( Base `  f )
2825, 2, 27wsbc 3004 . . 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 14076 . . 3  class  Preset
3028, 21, 29crab 2560 . 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 ) ) }
311, 30wceq 1632 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 ) ) }
Colors of variables: wff set class
This definition is referenced by:  isdrs  14084
  Copyright terms: Public domain W3C validator