Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-po GIF version

Definition df-po 4061
 Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. (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 4059 . 2 wff 𝑅 Po 𝐴
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1258 . . . . . . . 8 class 𝑥
65, 5, 2wbr 3792 . . . . . . 7 wff 𝑥𝑅𝑥
76wn 3 . . . . . 6 wff ¬ 𝑥𝑅𝑥
8 vy . . . . . . . . . 10 setvar 𝑦
98cv 1258 . . . . . . . . 9 class 𝑦
105, 9, 2wbr 3792 . . . . . . . 8 wff 𝑥𝑅𝑦
11 vz . . . . . . . . . 10 setvar 𝑧
1211cv 1258 . . . . . . . . 9 class 𝑧
139, 12, 2wbr 3792 . . . . . . . 8 wff 𝑦𝑅𝑧
1410, 13wa 101 . . . . . . 7 wff (𝑥𝑅𝑦𝑦𝑅𝑧)
155, 12, 2wbr 3792 . . . . . . 7 wff 𝑥𝑅𝑧
1614, 15wi 4 . . . . . 6 wff ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
177, 16wa 101 . . . . 5 wff 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1817, 11, 1wral 2323 . . . 4 wff 𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1918, 8, 1wral 2323 . . 3 wff 𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
2019, 4, 1wral 2323 . 2 wff 𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
213, 20wb 102 1 wff (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
 Colors of variables: wff set class This definition is referenced by:  poss  4063  poeq1  4064  nfpo  4066  pocl  4068  ispod  4069  po0  4076  poinxp  4437  posng  4440  cnvpom  4888  isopolem  5489  poxp  5881
 Copyright terms: Public domain W3C validator