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

Definition df-drs 14063
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 14061 . 2  class Dirset
2 vb . . . . . . . 8  set  b
32cv 1622 . . . . . . 7  class  b
4 c0 3455 . . . . . . 7  class  (/)
53, 4wne 2446 . . . . . 6  wff  b  =/=  (/)
6 vx . . . . . . . . . . . 12  set  x
76cv 1622 . . . . . . . . . . 11  class  x
8 vz . . . . . . . . . . . 12  set  z
98cv 1622 . . . . . . . . . . 11  class  z
10 vr . . . . . . . . . . . 12  set  r
1110cv 1622 . . . . . . . . . . 11  class  r
127, 9, 11wbr 4023 . . . . . . . . . 10  wff  x r z
13 vy . . . . . . . . . . . 12  set  y
1413cv 1622 . . . . . . . . . . 11  class  y
1514, 9, 11wbr 4023 . . . . . . . . . 10  wff  y r z
1612, 15wa 358 . . . . . . . . 9  wff  ( x r z  /\  y
r z )
1716, 8, 3wrex 2544 . . . . . . . 8  wff  E. z  e.  b  ( x
r z  /\  y
r z )
1817, 13, 3wral 2543 . . . . . . 7  wff  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z )
1918, 6, 3wral 2543 . . . . . 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 1622 . . . . . 6  class  f
23 cple 13215 . . . . . 6  class  le
2422, 23cfv 5255 . . . . 5  class  ( le
`  f )
2520, 10, 24wsbc 2991 . . . 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 13148 . . . . 5  class  Base
2722, 26cfv 5255 . . . 4  class  ( Base `  f )
2825, 2, 27wsbc 2991 . . 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 14060 . . 3  class  Preset
3028, 21, 29crab 2547 . 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 1623 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  14068
  Copyright terms: Public domain W3C validator