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

Definition df-po 4644
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 22252). (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 4642 . 2
4 vx . . . . . . . . 9
54cv 1661 . . . . . . . 8
65, 5, 2wbr 4302 . . . . . . 7
76wn 3 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1661 . . . . . . . . 9
105, 9, 2wbr 4302 . . . . . . . 8
11 vz . . . . . . . . . 10
1211cv 1661 . . . . . . . . 9
139, 12, 2wbr 4302 . . . . . . . 8
1410, 13wa 360 . . . . . . 7
155, 12, 2wbr 4302 . . . . . . 7
1614, 15wi 4 . . . . . 6
177, 16wa 360 . . . . 5
1817, 11, 1wral 2751 . . . 4
1918, 8, 1wral 2751 . . 3
2019, 4, 1wral 2751 . 2
213, 20wb 178 1
Colors of variables: wff set class
This definition is referenced by:  poss  4646  poeq1  4647  nfpo  4649  pocl  4651  ispod  4652  po0  4659  poinxp  4906  posn  4911  cnvpo  5374  isopolem  6010  porpss  6330  dfwe2  6358  poxp  6641  dfso3  26007  dfpo2  26208  elpotr  26238  poseq  26358
  Copyright terms: Public domain W3C validator