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

Definition df-po 4506
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 21748). (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 4504 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  set  x
54cv 1652 . . . . . . . 8  class  x
65, 5, 2wbr 4215 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  set  y
98cv 1652 . . . . . . . . 9  class  y
105, 9, 2wbr 4215 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  set  z
1211cv 1652 . . . . . . . . 9  class  z
139, 12, 2wbr 4215 . . . . . . . 8  wff  y R z
1410, 13wa 360 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 4215 . . . . . . 7  wff  x R z
1614, 15wi 4 . . . . . 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 2707 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2707 . . 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 2707 . 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  4508  poeq1  4509  nfpo  4511  pocl  4513  ispod  4514  po0  4521  dfwe2  4765  poinxp  4944  posn  4949  cnvpo  5413  isopolem  6068  poxp  6461  porpss  6529  dfso3  25182  dfpo2  25383  elpotr  25413  poseq  25533
  Copyright terms: Public domain W3C validator