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

Definition df-po 5587
Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. For example, < Po ℝ is true, while ≤ Po ℝ is false (ex-po 29668). (Contributed by NM, 16-Mar-1997.)
Assertion
Ref Expression
df-po (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑅   𝑥,𝐴,𝑦,𝑧

Detailed syntax breakdown of Definition df-po
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wpo 5585 . 2 wff 𝑅 Po 𝐴
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1541 . . . . . . . 8 class 𝑥
65, 5, 2wbr 5147 . . . . . . 7 wff 𝑥𝑅𝑥
76wn 3 . . . . . 6 wff ¬ 𝑥𝑅𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1541 . . . . . . . . 9 class 𝑦
105, 9, 2wbr 5147 . . . . . . . 8 wff 𝑥𝑅𝑦
11 vz . . . . . . . . . 10 setvar 𝑧
1211cv 1541 . . . . . . . . 9 class 𝑧
139, 12, 2wbr 5147 . . . . . . . 8 wff 𝑦𝑅𝑧
1410, 13wa 397 . . . . . . 7 wff (𝑥𝑅𝑦𝑦𝑅𝑧)
155, 12, 2wbr 5147 . . . . . . 7 wff 𝑥𝑅𝑧
1614, 15wi 4 . . . . . 6 wff ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
177, 16wa 397 . . . . 5 wff 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1817, 11, 1wral 3062 . . . 4 wff 𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1918, 8, 1wral 3062 . . 3 wff 𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
2019, 4, 1wral 3062 . 2 wff 𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
213, 20wb 205 1 wff (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Colors of variables: wff setvar class
This definition is referenced by:  poss  5589  poeq1  5590  nfpo  5592  pocl  5594  poclOLD  5595  ispod  5596  po0  5604  poinxp  5754  posn  5759  cnvpo  6283  dfpo2  6292  isopolem  7337  porpss  7712  dfwe2  7756  epweon  7757  poxp  8109  poseq  8139  dfso3  34627  elpotr  34691
  Copyright terms: Public domain W3C validator