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 5179
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 27595). (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 5177 . 2 wff 𝑅 Po 𝐴
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1623 . . . . . . . 8 class 𝑥
65, 5, 2wbr 4796 . . . . . . 7 wff 𝑥𝑅𝑥
76wn 3 . . . . . 6 wff ¬ 𝑥𝑅𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1623 . . . . . . . . 9 class 𝑦
105, 9, 2wbr 4796 . . . . . . . 8 wff 𝑥𝑅𝑦
11 vz . . . . . . . . . 10 setvar 𝑧
1211cv 1623 . . . . . . . . 9 class 𝑧
139, 12, 2wbr 4796 . . . . . . . 8 wff 𝑦𝑅𝑧
1410, 13wa 383 . . . . . . 7 wff (𝑥𝑅𝑦𝑦𝑅𝑧)
155, 12, 2wbr 4796 . . . . . . 7 wff 𝑥𝑅𝑧
1614, 15wi 4 . . . . . 6 wff ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
177, 16wa 383 . . . . 5 wff 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1817, 11, 1wral 3042 . . . 4 wff 𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1918, 8, 1wral 3042 . . 3 wff 𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
2019, 4, 1wral 3042 . 2 wff 𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
213, 20wb 196 1 wff (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Colors of variables: wff setvar class
This definition is referenced by:  poss  5181  poeq1  5182  nfpo  5184  pocl  5186  ispod  5187  po0  5194  poinxp  5331  posn  5336  cnvpo  5826  isopolem  6750  porpss  7098  dfwe2  7138  poxp  7449  dfso3  31900  dfpo2  31944  elpotr  31983  poseq  32051
  Copyright terms: Public domain W3C validator