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

Definition df-po 4251
Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression  R  Po  A means  R is a partial order on  A. For example,  <  Po  RR is true, while  <_  Po  RR is false (ex-po 20730). (Contributed by NM, 16-Mar-1997.)
Assertion
Ref Expression
df-po  |-  ( R  Po  A  <->  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) )
Distinct variable groups:    x, y,
z, R    x, A, y, z

Detailed syntax breakdown of Definition df-po
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wpo 4249 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  set  x
54cv 1618 . . . . . . . 8  class  x
65, 5, 2wbr 3963 . . . . . . 7  wff  x R x
76wn 5 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  set  y
98cv 1618 . . . . . . . . 9  class  y
105, 9, 2wbr 3963 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  set  z
1211cv 1618 . . . . . . . . 9  class  z
139, 12, 2wbr 3963 . . . . . . . 8  wff  y R z
1410, 13wa 360 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 3963 . . . . . . 7  wff  x R z
1614, 15wi 6 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
177, 16wa 360 . . . . 5  wff  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) )
1817, 11, 1wral 2516 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2516 . . 3  wff  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
2019, 4, 1wral 2516 . 2  wff  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
213, 20wb 178 1  wff  ( R  Po  A  <->  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) )
Colors of variables: wff set class
This definition is referenced by:  poss  4253  poeq1  4254  nfpo  4256  pocl  4258  ispod  4259  po0  4266  dfwe2  4510  poinxp  4706  posn  4711  cnvpo  5165  isopolem  5741  poxp  6126  porpss  6180  dfso3  23411  dfpo2  23448  elpotr  23471  poseq  23587
  Copyright terms: Public domain W3C validator