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

Definition df-tsr 16390
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 16388 . 2  class  TosetRel
2 vr . . . . . . 7  setvar  r
32cv 1436 . . . . . 6  class  r
43cdm 4796 . . . . 5  class  dom  r
54, 4cxp 4794 . . . 4  class  ( dom  r  X.  dom  r
)
63ccnv 4795 . . . . 5  class  `' r
73, 6cun 3377 . . . 4  class  ( r  u.  `' r )
85, 7wss 3379 . . 3  wff  ( dom  r  X.  dom  r
)  C_  ( r  u.  `' r )
9 cps 16387 . . 3  class  PosetRel
108, 2, 9crab 2718 . 2  class  { r  e.  PosetRel  |  ( dom  r  X.  dom  r ) 
C_  ( r  u.  `' r ) }
111, 10wceq 1437 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  16406
  Copyright terms: Public domain W3C validator