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

Definition df-ps 14306
Description: Define the class of all posets (partially ordered sets) with weak ordering (e.g. "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.)
Assertion
Ref Expression
df-ps  |-  PosetRel  =  {
r  |  ( Rel  r  /\  ( r  o.  r )  C_  r  /\  ( r  i^i  `' r )  =  (  _I  |`  U. U. r ) ) }

Detailed syntax breakdown of Definition df-ps
StepHypRef Expression
1 cps 14301 . 2  class  PosetRel
2 vr . . . . . 6  set  r
32cv 1622 . . . . 5  class  r
43wrel 4694 . . . 4  wff  Rel  r
53, 3ccom 4693 . . . . 5  class  ( r  o.  r )
65, 3wss 3152 . . . 4  wff  ( r  o.  r )  C_  r
73ccnv 4688 . . . . . 6  class  `' r
83, 7cin 3151 . . . . 5  class  ( r  i^i  `' r )
9 cid 4304 . . . . . 6  class  _I
103cuni 3827 . . . . . . 7  class  U. r
1110cuni 3827 . . . . . 6  class  U. U. r
129, 11cres 4691 . . . . 5  class  (  _I  |`  U. U. r )
138, 12wceq 1623 . . . 4  wff  ( r  i^i  `' r )  =  (  _I  |`  U. U. r )
144, 6, 13w3a 934 . . 3  wff  ( Rel  r  /\  ( r  o.  r )  C_  r  /\  ( r  i^i  `' r )  =  (  _I  |`  U. U. r ) )
1514, 2cab 2269 . 2  class  { r  |  ( Rel  r  /\  ( r  o.  r
)  C_  r  /\  ( r  i^i  `' r )  =  (  _I  |`  U. U. r
) ) }
161, 15wceq 1623 1  wff  PosetRel  =  {
r  |  ( Rel  r  /\  ( r  o.  r )  C_  r  /\  ( r  i^i  `' r )  =  (  _I  |`  U. U. r ) ) }
Colors of variables: wff set class
This definition is referenced by:  isps  14311  posprsr  25240  dfps2  25289
  Copyright terms: Public domain W3C validator