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

Definition df-tsr 14323
Description: Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.)
Assertion
Ref Expression
df-tsr  |-  TosetRel  =  {
r  e.  PosetRel  |  ( dom  r  X.  dom  r )  C_  (
r  u.  `' r ) }

Detailed syntax breakdown of Definition df-tsr
StepHypRef Expression
1 ctsr 14318 . 2  class  TosetRel
2 vr . . . . . . 7  set  r
32cv 1631 . . . . . 6  class  r
43cdm 4705 . . . . 5  class  dom  r
54, 4cxp 4703 . . . 4  class  ( dom  r  X.  dom  r
)
63ccnv 4704 . . . . 5  class  `' r
73, 6cun 3163 . . . 4  class  ( r  u.  `' r )
85, 7wss 3165 . . 3  wff  ( dom  r  X.  dom  r
)  C_  ( r  u.  `' r )
9 cps 14317 . . 3  class  PosetRel
108, 2, 9crab 2560 . 2  class  { r  e.  PosetRel  |  ( dom  r  X.  dom  r ) 
C_  ( r  u.  `' r ) }
111, 10wceq 1632 1  wff  TosetRel  =  {
r  e.  PosetRel  |  ( dom  r  X.  dom  r )  C_  (
r  u.  `' r ) }
Colors of variables: wff set class
This definition is referenced by:  istsr  14342
  Copyright terms: Public domain W3C validator