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

Definition df-po 5035
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 27292). (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 5033 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  setvar  x
54cv 1482 . . . . . . . 8  class  x
65, 5, 2wbr 4653 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  setvar  y
98cv 1482 . . . . . . . . 9  class  y
105, 9, 2wbr 4653 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  setvar  z
1211cv 1482 . . . . . . . . 9  class  z
139, 12, 2wbr 4653 . . . . . . . 8  wff  y R z
1410, 13wa 384 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 4653 . . . . . . 7  wff  x R z
1614, 15wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
177, 16wa 384 . . . . 5  wff  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) )
1817, 11, 1wral 2912 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2912 . . 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 2912 . 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 196 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 setvar class
This definition is referenced by:  poss  5037  poeq1  5038  nfpo  5040  pocl  5042  ispod  5043  po0  5050  poinxp  5182  posn  5187  cnvpo  5673  isopolem  6595  porpss  6941  dfwe2  6981  poxp  7289  dfso3  31601  dfpo2  31645  elpotr  31686  poseq  31750
  Copyright terms: Public domain W3C validator