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 5468
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 28142). (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 5466 . 2 wff 𝑅 Po 𝐴
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1527 . . . . . . . 8 class 𝑥
65, 5, 2wbr 5058 . . . . . . 7 wff 𝑥𝑅𝑥
76wn 3 . . . . . 6 wff ¬ 𝑥𝑅𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1527 . . . . . . . . 9 class 𝑦
105, 9, 2wbr 5058 . . . . . . . 8 wff 𝑥𝑅𝑦
11 vz . . . . . . . . . 10 setvar 𝑧
1211cv 1527 . . . . . . . . 9 class 𝑧
139, 12, 2wbr 5058 . . . . . . . 8 wff 𝑦𝑅𝑧
1410, 13wa 396 . . . . . . 7 wff (𝑥𝑅𝑦𝑦𝑅𝑧)
155, 12, 2wbr 5058 . . . . . . 7 wff 𝑥𝑅𝑧
1614, 15wi 4 . . . . . 6 wff ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
177, 16wa 396 . . . . 5 wff 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1817, 11, 1wral 3138 . . . 4 wff 𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1918, 8, 1wral 3138 . . 3 wff 𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
2019, 4, 1wral 3138 . 2 wff 𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
213, 20wb 207 1 wff (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Colors of variables: wff setvar class
This definition is referenced by:  poss  5470  poeq1  5471  nfpo  5473  pocl  5475  ispod  5476  po0  5484  poinxp  5626  posn  5631  cnvpo  6132  isopolem  7087  porpss  7442  dfwe2  7484  poxp  7813  dfso3  32848  dfpo2  32889  elpotr  32924  poseq  32993
  Copyright terms: Public domain W3C validator