ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-po Unicode version

Definition df-po 4060
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. (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 4058 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  setvar  x
54cv 1258 . . . . . . . 8  class  x
65, 5, 2wbr 3791 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  setvar  y
98cv 1258 . . . . . . . . 9  class  y
105, 9, 2wbr 3791 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  setvar  z
1211cv 1258 . . . . . . . . 9  class  z
139, 12, 2wbr 3791 . . . . . . . 8  wff  y R z
1410, 13wa 101 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 3791 . . . . . . 7  wff  x R z
1614, 15wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
177, 16wa 101 . . . . 5  wff  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) )
1817, 11, 1wral 2323 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2323 . . 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 2323 . 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 102 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  4062  poeq1  4063  nfpo  4065  pocl  4067  ispod  4068  po0  4075  poinxp  4436  posng  4439  cnvpom  4887  isopolem  5488  poxp  5880
  Copyright terms: Public domain W3C validator