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

Definition df-po 4023
Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po A means 𝑅 is a partial order on A. (Contributed by NM, 16-Mar-1997.)
Assertion
Ref Expression
df-po (𝑅 Po Ax A y A z Ax𝑅x ((x𝑅y y𝑅z) → x𝑅z)))
Distinct variable groups:   x,y,z,𝑅   x,A,y,z

Detailed syntax breakdown of Definition df-po
StepHypRef Expression
1 cA . . 3 class A
2 cR . . 3 class 𝑅
31, 2wpo 4021 . 2 wff 𝑅 Po A
4 vx . . . . . . . . 9 setvar x
54cv 1241 . . . . . . . 8 class x
65, 5, 2wbr 3754 . . . . . . 7 wff x𝑅x
76wn 3 . . . . . 6 wff ¬ x𝑅x
8 vy . . . . . . . . . 10 setvar y
98cv 1241 . . . . . . . . 9 class y
105, 9, 2wbr 3754 . . . . . . . 8 wff x𝑅y
11 vz . . . . . . . . . 10 setvar z
1211cv 1241 . . . . . . . . 9 class z
139, 12, 2wbr 3754 . . . . . . . 8 wff y𝑅z
1410, 13wa 97 . . . . . . 7 wff (x𝑅y y𝑅z)
155, 12, 2wbr 3754 . . . . . . 7 wff x𝑅z
1614, 15wi 4 . . . . . 6 wff ((x𝑅y y𝑅z) → x𝑅z)
177, 16wa 97 . . . . 5 wff x𝑅x ((x𝑅y y𝑅z) → x𝑅z))
1817, 11, 1wral 2300 . . . 4 wff z Ax𝑅x ((x𝑅y y𝑅z) → x𝑅z))
1918, 8, 1wral 2300 . . 3 wff y A z Ax𝑅x ((x𝑅y y𝑅z) → x𝑅z))
2019, 4, 1wral 2300 . 2 wff x A y A z Ax𝑅x ((x𝑅y y𝑅z) → x𝑅z))
213, 20wb 98 1 wff (𝑅 Po Ax A y A z Ax𝑅x ((x𝑅y y𝑅z) → x𝑅z)))
Colors of variables: wff set class
This definition is referenced by:  poss  4025  poeq1  4026  nfpo  4028  pocl  4030  ispod  4031  po0  4038  poinxp  4351  posng  4354  cnvpom  4802  isopolem  5402  poxp  5791
  Copyright terms: Public domain W3C validator