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

Definition df-tsr 15473
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 15471 . 2  class  TosetRel
2 vr . . . . . . 7  setvar  r
32cv 1369 . . . . . 6  class  r
43cdm 4938 . . . . 5  class  dom  r
54, 4cxp 4936 . . . 4  class  ( dom  r  X.  dom  r
)
63ccnv 4937 . . . . 5  class  `' r
73, 6cun 3424 . . . 4  class  ( r  u.  `' r )
85, 7wss 3426 . . 3  wff  ( dom  r  X.  dom  r
)  C_  ( r  u.  `' r )
9 cps 15470 . . 3  class  PosetRel
108, 2, 9crab 2799 . 2  class  { r  e.  PosetRel  |  ( dom  r  X.  dom  r ) 
C_  ( r  u.  `' r ) }
111, 10wceq 1370 1  wff  TosetRel  =  {
r  e.  PosetRel  |  ( dom  r  X.  dom  r )  C_  (
r  u.  `' r ) }
Colors of variables: wff setvar class
This definition is referenced by:  istsr  15489
  Copyright terms: Public domain W3C validator