Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prs Unicode version

Definition df-prs 25223
Description: Define the class of all presets. A preset is a transitive and reflexive relation. ("preset" is the short for preordered set.) (Contributed by FL, 1-May-2011.)
Assertion
Ref Expression
df-prs  |- PresetRel  =  {
r  |  ( Rel  r  /\  ( r  o.  r )  C_  r  /\  (  _I  |`  U. U. r )  C_  r
) }

Detailed syntax breakdown of Definition df-prs
StepHypRef Expression
1 cpresetrel 25215 . 2  class PresetRel
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
7 cid 4304 . . . . . 6  class  _I
83cuni 3827 . . . . . . 7  class  U. r
98cuni 3827 . . . . . 6  class  U. U. r
107, 9cres 4691 . . . . 5  class  (  _I  |`  U. U. r )
1110, 3wss 3152 . . . 4  wff  (  _I  |`  U. U. r ) 
C_  r
124, 6, 11w3a 934 . . 3  wff  ( Rel  r  /\  ( r  o.  r )  C_  r  /\  (  _I  |`  U. U. r )  C_  r
)
1312, 2cab 2269 . 2  class  { r  |  ( Rel  r  /\  ( r  o.  r
)  C_  r  /\  (  _I  |`  U. U. r )  C_  r
) }
141, 13wceq 1623 1  wff PresetRel  =  {
r  |  ( Rel  r  /\  ( r  o.  r )  C_  r  /\  (  _I  |`  U. U. r )  C_  r
) }
Colors of variables: wff set class
This definition is referenced by:  isprsr  25224  posprsr  25240
  Copyright terms: Public domain W3C validator