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

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

Detailed syntax breakdown of Definition df-po
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2wpo 4227 . 2
4 vx . . . . . . . . 9
54cv 1331 . . . . . . . 8
65, 5, 2wbr 3939 . . . . . . 7
76wn 3 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1331 . . . . . . . . 9
105, 9, 2wbr 3939 . . . . . . . 8
11 vz . . . . . . . . . 10
1211cv 1331 . . . . . . . . 9
139, 12, 2wbr 3939 . . . . . . . 8
1410, 13wa 103 . . . . . . 7
155, 12, 2wbr 3939 . . . . . . 7
1614, 15wi 4 . . . . . 6
177, 16wa 103 . . . . 5
1817, 11, 1wral 2418 . . . 4
1918, 8, 1wral 2418 . . 3
2019, 4, 1wral 2418 . 2
213, 20wb 104 1
 Colors of variables: wff set class This definition is referenced by:  poss  4231  poeq1  4232  nfpo  4234  pocl  4236  ispod  4237  po0  4244  poinxp  4620  posng  4623  cnvpom  5093  isopolem  5735  poxp  6141
 Copyright terms: Public domain W3C validator