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

Definition df-toset 14140
Description: Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014.)
Assertion
Ref Expression
df-toset  |- Toset  =  {
f  e.  Poset  |  [. ( Base `  f )  /  b ]. [. ( le `  f )  / 
r ]. A. x  e.  b  A. y  e.  b  ( x r y  \/  y r x ) }
Distinct variable group:    f, b, r, x, y

Detailed syntax breakdown of Definition df-toset
StepHypRef Expression
1 ctos 14139 . 2  class Toset
2 vx . . . . . . . . . 10  set  x
32cv 1622 . . . . . . . . 9  class  x
4 vy . . . . . . . . . 10  set  y
54cv 1622 . . . . . . . . 9  class  y
6 vr . . . . . . . . . 10  set  r
76cv 1622 . . . . . . . . 9  class  r
83, 5, 7wbr 4023 . . . . . . . 8  wff  x r y
95, 3, 7wbr 4023 . . . . . . . 8  wff  y r x
108, 9wo 357 . . . . . . 7  wff  ( x r y  \/  y
r x )
11 vb . . . . . . . 8  set  b
1211cv 1622 . . . . . . 7  class  b
1310, 4, 12wral 2543 . . . . . 6  wff  A. y  e.  b  ( x
r y  \/  y
r x )
1413, 2, 12wral 2543 . . . . 5  wff  A. x  e.  b  A. y  e.  b  ( x
r y  \/  y
r x )
15 vf . . . . . . 7  set  f
1615cv 1622 . . . . . 6  class  f
17 cple 13215 . . . . . 6  class  le
1816, 17cfv 5255 . . . . 5  class  ( le
`  f )
1914, 6, 18wsbc 2991 . . . 4  wff  [. ( le `  f )  / 
r ]. A. x  e.  b  A. y  e.  b  ( x r y  \/  y r x )
20 cbs 13148 . . . . 5  class  Base
2116, 20cfv 5255 . . . 4  class  ( Base `  f )
2219, 11, 21wsbc 2991 . . 3  wff  [. ( Base `  f )  / 
b ]. [. ( le
`  f )  / 
r ]. A. x  e.  b  A. y  e.  b  ( x r y  \/  y r x )
23 cpo 14074 . . 3  class  Poset
2422, 15, 23crab 2547 . 2  class  { f  e.  Poset  |  [. ( Base `  f )  / 
b ]. [. ( le
`  f )  / 
r ]. A. x  e.  b  A. y  e.  b  ( x r y  \/  y r x ) }
251, 24wceq 1623 1  wff Toset  =  {
f  e.  Poset  |  [. ( Base `  f )  /  b ]. [. ( le `  f )  / 
r ]. A. x  e.  b  A. y  e.  b  ( x r y  \/  y r x ) }
Colors of variables: wff set class
This definition is referenced by:  istos  14141
  Copyright terms: Public domain W3C validator