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

Definition df-po 4314
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 20822). (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 4312 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  set  x
54cv 1622 . . . . . . . 8  class  x
65, 5, 2wbr 4023 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  set  y
98cv 1622 . . . . . . . . 9  class  y
105, 9, 2wbr 4023 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  set  z
1211cv 1622 . . . . . . . . 9  class  z
139, 12, 2wbr 4023 . . . . . . . 8  wff  y R z
1410, 13wa 358 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 4023 . . . . . . 7  wff  x R z
1614, 15wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
177, 16wa 358 . . . . 5  wff  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) )
1817, 11, 1wral 2543 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2543 . . 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 2543 . 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 176 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  4316  poeq1  4317  nfpo  4319  pocl  4321  ispod  4322  po0  4329  dfwe2  4573  poinxp  4753  posn  4758  cnvpo  5213  isopolem  5842  poxp  6227  porpss  6281  dfso3  24074  dfpo2  24112  elpotr  24137  poseq  24253
  Copyright terms: Public domain W3C validator