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

Definition df-po 4286
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 20766). (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 4284 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  set  x
54cv 1618 . . . . . . . 8  class  x
65, 5, 2wbr 3997 . . . . . . 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 3997 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  set  z
1211cv 1618 . . . . . . . . 9  class  z
139, 12, 2wbr 3997 . . . . . . . 8  wff  y R z
1410, 13wa 360 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 3997 . . . . . . 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 2518 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2518 . . 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 2518 . 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  4288  poeq1  4289  nfpo  4291  pocl  4293  ispod  4294  po0  4301  dfwe2  4545  poinxp  4741  posn  4746  cnvpo  5200  isopolem  5776  poxp  6161  porpss  6215  dfso3  23447  dfpo2  23484  elpotr  23507  poseq  23623
  Copyright terms: Public domain W3C validator