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

Definition df-po 4079
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 4077 . 2  wff  R  Po  A
4 vx . . . . . . . . 9  setvar  x
54cv 1284 . . . . . . . 8  class  x
65, 5, 2wbr 3805 . . . . . . 7  wff  x R x
76wn 3 . . . . . 6  wff  -.  x R x
8 vy . . . . . . . . . 10  setvar  y
98cv 1284 . . . . . . . . 9  class  y
105, 9, 2wbr 3805 . . . . . . . 8  wff  x R y
11 vz . . . . . . . . . 10  setvar  z
1211cv 1284 . . . . . . . . 9  class  z
139, 12, 2wbr 3805 . . . . . . . 8  wff  y R z
1410, 13wa 102 . . . . . . 7  wff  ( x R y  /\  y R z )
155, 12, 2wbr 3805 . . . . . . 7  wff  x R z
1614, 15wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
177, 16wa 102 . . . . 5  wff  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) )
1817, 11, 1wral 2353 . . . 4  wff  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) )
1918, 8, 1wral 2353 . . 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 2353 . 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 103 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  4081  poeq1  4082  nfpo  4084  pocl  4086  ispod  4087  po0  4094  poinxp  4455  posng  4458  cnvpom  4910  isopolem  5513  poxp  5905
  Copyright terms: Public domain W3C validator