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

Definition df-po 4033
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 4031 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  setvar  x
54cv 1242 . . . . . . . 8  class  x
65, 5, 2wbr 3764 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  setvar  y
98cv 1242 . . . . . . . . 9  class  y
105, 9, 2wbr 3764 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  setvar  z
1211cv 1242 . . . . . . . . 9  class  z
139, 12, 2wbr 3764 . . . . . . . 8  wff  y R z
1410, 13wa 97 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 3764 . . . . . . 7  wff  x R z
1614, 15wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
177, 16wa 97 . . . . 5  wff  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) )
1817, 11, 1wral 2306 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2306 . . 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 2306 . 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 98 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  4035  poeq1  4036  nfpo  4038  pocl  4040  ispod  4041  po0  4048  poinxp  4409  posng  4412  cnvpom  4860  isopolem  5461  poxp  5853
  Copyright terms: Public domain W3C validator