Definition df-po 4051

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 4049	. 2 wff R Po A
4		vx	. . . . . . . . 9 setvar x
5	4	cv 1283	. . . . . . . 8 class x
6	5, 5, 2	wbr 3785	. . . . . . 7 wff x R x
7	6	wn 3	. . . . . 6 wff -. x R x
8		vy	. . . . . . . . . 10 setvar y
9	8	cv 1283	. . . . . . . . 9 class y
10	5, 9, 2	wbr 3785	. . . . . . . 8 wff x R y
11		vz	. . . . . . . . . 10 setvar z
12	11	cv 1283	. . . . . . . . 9 class z
13	9, 12, 2	wbr 3785	. . . . . . . 8 wff y R z
14	10, 13	wa 102	. . . . . . 7 wff ( x R y /\ y R z )
15	5, 12, 2	wbr 3785	. . . . . . 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 102	. . . . 5 wff ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
18	17, 11, 1	wral 2348	. . . 4 wff A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
19	18, 8, 1	wral 2348	. . 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 2348	. 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 103	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  4053  poeq1  4054  nfpo  4056  pocl  4058  ispod  4059  po0  4066  poinxp  4427  posng  4430  cnvpom  4880  isopolem  5481  poxp  5873