Definition df-po 4281

Description: Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression R Po A means R is a partial order on A. (Contributed by NM, 16-Mar-1997.)

Assertion

Ref	Expression
df-po	|- ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )

Distinct variable groups:   x, y, z, R   x, A, y, z

Detailed syntax breakdown of Definition df-po

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wpo 4279	. 2 wff R Po A
4		vx	. . . . . . . . 9 setvar x
5	4	cv 1347	. . . . . . . 8 class x
6	5, 5, 2	wbr 3989	. . . . . . 7 wff x R x
7	6	wn 3	. . . . . 6 wff -. x R x
8		vy	. . . . . . . . . 10 setvar y
9	8	cv 1347	. . . . . . . . 9 class y
10	5, 9, 2	wbr 3989	. . . . . . . 8 wff x R y
11		vz	. . . . . . . . . 10 setvar z
12	11	cv 1347	. . . . . . . . 9 class z
13	9, 12, 2	wbr 3989	. . . . . . . 8 wff y R z
14	10, 13	wa 103	. . . . . . 7 wff ( x R y /\ y R z )
15	5, 12, 2	wbr 3989	. . . . . . 7 wff x R z
16	14, 15	wi 4	. . . . . 6 wff ( ( x R y /\ y R z ) -> x R z )
17	7, 16	wa 103	. . . . 5 wff ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
18	17, 11, 1	wral 2448	. . . 4 wff A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
19	18, 8, 1	wral 2448	. . 3 wff A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
20	19, 4, 1	wral 2448	. 2 wff A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
21	3, 20	wb 104	1 wff ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )

This definition is referenced by:  poss  4283  poeq1  4284  nfpo  4286  pocl  4288  ispod  4289  po0  4296  poinxp  4680  posng  4683  cnvpom  5153  isopolem  5801  poxp  6211