MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-po Unicode version

Definition df-po 4662
Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression means is a partial order on . For example, is true, while is false (ex-po 22764). (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 4660 . 2
4 vx . . . . . . . . 9
54cv 1669 . . . . . . . 8
65, 5, 2wbr 4318 . . . . . . 7
76wn 3 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1669 . . . . . . . . 9
105, 9, 2wbr 4318 . . . . . . . 8
11 vz . . . . . . . . . 10
1211cv 1669 . . . . . . . . 9
139, 12, 2wbr 4318 . . . . . . . 8
1410, 13wa 360 . . . . . . 7
155, 12, 2wbr 4318 . . . . . . 7
1614, 15wi 4 . . . . . 6
177, 16wa 360 . . . . 5
1817, 11, 1wral 2759 . . . 4
1918, 8, 1wral 2759 . . 3
2019, 4, 1wral 2759 . 2
213, 20wb 178 1
Colors of variables: wff set class
This definition is referenced by:  poss  4664  poeq1  4665  nfpo  4667  pocl  4669  ispod  4670  po0  4677  poinxp  4924  posn  4929  cnvpo  5395  isopolem  6046  porpss  6374  dfwe2  6403  poxp  6690  dfso3  26516  dfpo2  26717  elpotr  26747  poseq  26867
  Copyright terms: Public domain W3C validator