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

Definition df-po 4463
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 21696). (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 4461 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  set  x
54cv 1648 . . . . . . . 8  class  x
65, 5, 2wbr 4172 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  set  y
98cv 1648 . . . . . . . . 9  class  y
105, 9, 2wbr 4172 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  set  z
1211cv 1648 . . . . . . . . 9  class  z
139, 12, 2wbr 4172 . . . . . . . 8  wff  y R z
1410, 13wa 359 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 4172 . . . . . . 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 2666 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2666 . . 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 2666 . 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  4465  poeq1  4466  nfpo  4468  pocl  4470  ispod  4471  po0  4478  dfwe2  4721  poinxp  4900  posn  4905  cnvpo  5369  isopolem  6024  poxp  6417  porpss  6485  dfso3  25130  dfpo2  25326  elpotr  25351  poseq  25467
  Copyright terms: Public domain W3C validator