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

Definition df-po 4495
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 21735). (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 4493 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  set  x
54cv 1651 . . . . . . . 8  class  x
65, 5, 2wbr 4204 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  set  y
98cv 1651 . . . . . . . . 9  class  y
105, 9, 2wbr 4204 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  set  z
1211cv 1651 . . . . . . . . 9  class  z
139, 12, 2wbr 4204 . . . . . . . 8  wff  y R z
1410, 13wa 359 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 4204 . . . . . . 7  wff  x R z
1614, 15wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
177, 16wa 359 . . . . 5  wff  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) )
1817, 11, 1wral 2697 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2697 . . 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 2697 . 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 177 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  4497  poeq1  4498  nfpo  4500  pocl  4502  ispod  4503  po0  4510  dfwe2  4754  poinxp  4933  posn  4938  cnvpo  5402  isopolem  6057  poxp  6450  porpss  6518  dfso3  25169  dfpo2  25370  elpotr  25400  poseq  25520
  Copyright terms: Public domain W3C validator