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

Definition df-po 4458
 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 21663). (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 4456 . 2
4 vx . . . . . . . . 9
54cv 1648 . . . . . . . 8
65, 5, 2wbr 4167 . . . . . . 7
76wn 3 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1648 . . . . . . . . 9
105, 9, 2wbr 4167 . . . . . . . 8
11 vz . . . . . . . . . 10
1211cv 1648 . . . . . . . . 9
139, 12, 2wbr 4167 . . . . . . . 8
1410, 13wa 359 . . . . . . 7
155, 12, 2wbr 4167 . . . . . . 7
1614, 15wi 4 . . . . . 6
177, 16wa 359 . . . . 5
1817, 11, 1wral 2663 . . . 4
1918, 8, 1wral 2663 . . 3
2019, 4, 1wral 2663 . 2
213, 20wb 177 1
 Colors of variables: wff set class This definition is referenced by:  poss  4460  poeq1  4461  nfpo  4463  pocl  4465  ispod  4466  po0  4473  dfwe2  4716  poinxp  4895  posn  4900  cnvpo  5364  isopolem  6018  poxp  6408  porpss  6476  dfso3  25099  dfpo2  25295  elpotr  25320  poseq  25436
 Copyright terms: Public domain W3C validator