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

Definition df-po 4207
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 20635). (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 4205 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  set  x
54cv 1618 . . . . . . . 8  class  x
65, 5, 2wbr 3920 . . . . . . 7  wff  x R x
76wn 5 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  set  y
98cv 1618 . . . . . . . . 9  class  y
105, 9, 2wbr 3920 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  set  z
1211cv 1618 . . . . . . . . 9  class  z
139, 12, 2wbr 3920 . . . . . . . 8  wff  y R z
1410, 13wa 360 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 3920 . . . . . . 7  wff  x R z
1614, 15wi 6 . . . . . 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 2509 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2509 . . 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 2509 . 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  4209  poeq1  4210  nfpo  4212  pocl  4214  ispod  4215  po0  4222  dfwe2  4464  poinxp  4660  posn  4665  cnvpo  5119  isopolem  5694  poxp  6079  porpss  6133  dfso3  23245  dfpo2  23282  elpotr  23305  poseq  23421
  Copyright terms: Public domain W3C validator