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

Definition df-po 4024
Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression  R  Po means  R is a partial order on . (Contributed by NM, 16-Mar-1997.)
Assertion
Ref Expression
df-po  R  Po  R  R  R  R
Distinct variable groups:   ,,, R   ,,,

Detailed syntax breakdown of Definition df-po
StepHypRef Expression
1 cA . . 3
2 cR . . 3  R
31, 2wpo 4022 . 2  R  Po
4 vx . . . . . . . . 9  setvar
54cv 1241 . . . . . . . 8
65, 5, 2wbr 3755 . . . . . . 7  R
76wn 3 . . . . . 6  R
8 vy . . . . . . . . . 10  setvar
98cv 1241 . . . . . . . . 9
105, 9, 2wbr 3755 . . . . . . . 8  R
11 vz . . . . . . . . . 10  setvar
1211cv 1241 . . . . . . . . 9
139, 12, 2wbr 3755 . . . . . . . 8  R
1410, 13wa 97 . . . . . . 7  R  R
155, 12, 2wbr 3755 . . . . . . 7  R
1614, 15wi 4 . . . . . 6  R  R  R
177, 16wa 97 . . . . 5  R  R  R  R
1817, 11, 1wral 2300 . . . 4  R  R  R  R
1918, 8, 1wral 2300 . . 3  R  R  R  R
2019, 4, 1wral 2300 . 2  R  R  R  R
213, 20wb 98 1  R  Po  R  R  R  R
Colors of variables: wff set class
This definition is referenced by:  poss  4026  poeq1  4027  nfpo  4029  pocl  4031  ispod  4032  po0  4039  poinxp  4352  posng  4355  cnvpom  4803  isopolem  5404  poxp  5794
  Copyright terms: Public domain W3C validator