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

Definition df-po 4417
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 21254). (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 4415 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  set  x
54cv 1646 . . . . . . . 8  class  x
65, 5, 2wbr 4125 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  set  y
98cv 1646 . . . . . . . . 9  class  y
105, 9, 2wbr 4125 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  set  z
1211cv 1646 . . . . . . . . 9  class  z
139, 12, 2wbr 4125 . . . . . . . 8  wff  y R z
1410, 13wa 358 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 4125 . . . . . . 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 2628 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2628 . . 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 2628 . 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  4419  poeq1  4420  nfpo  4422  pocl  4424  ispod  4425  po0  4432  dfwe2  4676  poinxp  4856  posn  4861  cnvpo  5316  isopolem  5965  poxp  6355  porpss  6423  dfso3  24746  dfpo2  24938  elpotr  24963  poseq  25079
  Copyright terms: Public domain W3C validator