MPE Home 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  =  {
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 14376 . 2  class Dirset
2 vb . . . . . . . 8  set  b
32cv 1651 . . . . . . 7  class  b
4 c0 3620 . . . . . . 7  class  (/)
53, 4wne 2598 . . . . . 6  wff  b  =/=  (/)
6 vx . . . . . . . . . . . 12  set  x
76cv 1651 . . . . . . . . . . 11  class  x
8 vz . . . . . . . . . . . 12  set  z
98cv 1651 . . . . . . . . . . 11  class  z
10 vr . . . . . . . . . . . 12  set  r
1110cv 1651 . . . . . . . . . . 11  class  r
127, 9, 11wbr 4204 . . . . . . . . . 10  wff  x r z
13 vy . . . . . . . . . . . 12  set  y
1413cv 1651 . . . . . . . . . . 11  class  y
1514, 9, 11wbr 4204 . . . . . . . . . 10  wff  y r z
1612, 15wa 359 . . . . . . . . 9  wff  ( x r z  /\  y
r z )
1716, 8, 3wrex 2698 . . . . . . . 8  wff  E. z  e.  b  ( x
r z  /\  y
r z )
1817, 13, 3wral 2697 . . . . . . 7  wff  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z )
1918, 6, 3wral 2697 . . . . . 6  wff  A. x  e.  b  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z )
205, 19wa 359 . . . . 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 1651 . . . . . 6  class  f
23 cple 13528 . . . . . 6  class  le
2422, 23cfv 5446 . . . . 5  class  ( le
`  f )
2520, 10, 24wsbc 3153 . . . 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 13461 . . . . 5  class  Base
2722, 26cfv 5446 . . . 4  class  ( Base `  f )
2825, 2, 27wsbc 3153 . . 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 14375 . . 3  class  Preset
3028, 21, 29crab 2701 . 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 1652 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  14383
  Copyright terms: Public domain W3C validator