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 4948
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 26477). (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 4946 . 2 wff 𝑅 Po 𝐴
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1473 . . . . . . . 8 class 𝑥
65, 5, 2wbr 4577 . . . . . . 7 wff 𝑥𝑅𝑥
76wn 3 . . . . . 6 wff ¬ 𝑥𝑅𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1473 . . . . . . . . 9 class 𝑦
105, 9, 2wbr 4577 . . . . . . . 8 wff 𝑥𝑅𝑦
11 vz . . . . . . . . . 10 setvar 𝑧
1211cv 1473 . . . . . . . . 9 class 𝑧
139, 12, 2wbr 4577 . . . . . . . 8 wff 𝑦𝑅𝑧
1410, 13wa 382 . . . . . . 7 wff (𝑥𝑅𝑦𝑦𝑅𝑧)
155, 12, 2wbr 4577 . . . . . . 7 wff 𝑥𝑅𝑧
1614, 15wi 4 . . . . . 6 wff ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
177, 16wa 382 . . . . 5 wff 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1817, 11, 1wral 2895 . . . 4 wff 𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1918, 8, 1wral 2895 . . 3 wff 𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
2019, 4, 1wral 2895 . 2 wff 𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
213, 20wb 194 1 wff (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Colors of variables: wff setvar class
This definition is referenced by:  poss  4950  poeq1  4951  nfpo  4953  pocl  4955  ispod  4956  po0  4963  poinxp  5094  posn  5099  cnvpo  5575  isopolem  6472  porpss  6816  dfwe2  6850  poxp  7153  dfso3  30649  dfpo2  30691  elpotr  30723  poseq  30787
  Copyright terms: Public domain W3C validator