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

Definition df-po 4544
Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression means is a partial order on ?Error: < Po RR ^ This math symbol is not active (i.e. was not declared in this scope). ?Error: <_ Po RR ^^ This math symbol is not active (i.e. was not declared in this scope). . For example, Po is true, while Po is false (ex-po 21794). (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 4542 . 2
4 vx . . . . . . . . 9
54cv 1653 . . . . . . . 8
65, 5, 2wbr 4243 . . . . . . 7
76wn 3 . . . . . 6
8 vy . . . . . . . . . 10
98cv 1653 . . . . . . . . 9
105, 9, 2wbr 4243 . . . . . . . 8
11 vz . . . . . . . . . 10
1211cv 1653 . . . . . . . . 9
139, 12, 2wbr 4243 . . . . . . . 8
1410, 13wa 360 . . . . . . 7
155, 12, 2wbr 4243 . . . . . . 7
1614, 15wi 4 . . . . . 6
177, 16wa 360 . . . . 5
1817, 11, 1wral 2712 . . . 4
1918, 8, 1wral 2712 . . 3
2019, 4, 1wral 2712 . 2
213, 20wb 178 1
Colors of variables: wff set class
This definition is referenced by:  poss  4546  poeq1  4547  nfpo  4549  pocl  4551  ispod  4552  po0  4559  dfwe2  4803  poinxp  4981  posn  4986  cnvpo  5456  isopolem  6113  poxp  6508  porpss  6576  dfso3  25281  dfpo2  25482  elpotr  25512  poseq  25632
  Copyright terms: Public domain W3C validator