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

Definition df-po 4805
 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 25156). (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 4803 . 2
4 vx . . . . . . . . 9
54cv 1394 . . . . . . . 8
65, 5, 2wbr 4452 . . . . . . 7
76wn 3 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1394 . . . . . . . . 9
105, 9, 2wbr 4452 . . . . . . . 8
11 vz . . . . . . . . . 10
1211cv 1394 . . . . . . . . 9
139, 12, 2wbr 4452 . . . . . . . 8
1410, 13wa 369 . . . . . . 7
155, 12, 2wbr 4452 . . . . . . 7
1614, 15wi 4 . . . . . 6
177, 16wa 369 . . . . 5
1817, 11, 1wral 2807 . . . 4
1918, 8, 1wral 2807 . . 3
2019, 4, 1wral 2807 . 2
213, 20wb 184 1
 Colors of variables: wff setvar class This definition is referenced by:  poss  4807  poeq1  4808  nfpo  4810  pocl  4812  ispod  4813  po0  4820  poinxp  5068  posn  5073  cnvpo  5550  isopolem  6241  porpss  6584  dfwe2  6617  poxp  6912  dfso3  29097  dfpo2  29184  elpotr  29213  poseq  29333
 Copyright terms: Public domain W3C validator