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

Definition df-drs 15099
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 15097 . 2  class Dirset
2 vb . . . . . . . 8  setvar  b
32cv 1368 . . . . . . 7  class  b
4 c0 3637 . . . . . . 7  class  (/)
53, 4wne 2606 . . . . . 6  wff  b  =/=  (/)
6 vx . . . . . . . . . . . 12  setvar  x
76cv 1368 . . . . . . . . . . 11  class  x
8 vz . . . . . . . . . . . 12  setvar  z
98cv 1368 . . . . . . . . . . 11  class  z
10 vr . . . . . . . . . . . 12  setvar  r
1110cv 1368 . . . . . . . . . . 11  class  r
127, 9, 11wbr 4292 . . . . . . . . . 10  wff  x r z
13 vy . . . . . . . . . . . 12  setvar  y
1413cv 1368 . . . . . . . . . . 11  class  y
1514, 9, 11wbr 4292 . . . . . . . . . 10  wff  y r z
1612, 15wa 369 . . . . . . . . 9  wff  ( x r z  /\  y
r z )
1716, 8, 3wrex 2716 . . . . . . . 8  wff  E. z  e.  b  ( x
r z  /\  y
r z )
1817, 13, 3wral 2715 . . . . . . 7  wff  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z )
1918, 6, 3wral 2715 . . . . . 6  wff  A. x  e.  b  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z )
205, 19wa 369 . . . . 5  wff  ( b  =/=  (/)  /\  A. x  e.  b  A. y  e.  b  E. z  e.  b  ( x
r z  /\  y
r z ) )
21 vf . . . . . . 7  setvar  f
2221cv 1368 . . . . . 6  class  f
23 cple 14245 . . . . . 6  class  le
2422, 23cfv 5418 . . . . 5  class  ( le
`  f )
2520, 10, 24wsbc 3186 . . . 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 14174 . . . . 5  class  Base
2722, 26cfv 5418 . . . 4  class  ( Base `  f )
2825, 2, 27wsbc 3186 . . 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 15096 . . 3  class  Preset
3028, 21, 29crab 2719 . 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 1369 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 setvar class
This definition is referenced by:  isdrs  15104
  Copyright terms: Public domain W3C validator