Definition df-po

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 . For example, < Po RR is true, while <_ Po RR is false ( ex-po ). (Contributed by NM, 16-Mar-1997)

	Ref	Expression
Assertion	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 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1		cA	|- A
2	1 0	wpo	|- R Po A
3		vx	|- x
4		vy	|- y
5		vz	|- z
6	3	cv	|- x
7	6 6 0	wbr	|- x R x
8	7	wn	|- -. x R x
9	4	cv	|- y
10	6 9 0	wbr	|- x R y
11	5	cv	|- z
12	9 11 0	wbr	|- y R z
13	10 12	wa	|- ( x R y /\ y R z )
14	6 11 0	wbr	|- x R z
15	13 14	wi	|- ( ( x R y /\ y R z ) -> x R z )
16	8 15	wa	|- ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
17	16 5 1	wral	|- A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
18	17 4 1	wral	|- A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
19	18 3 1	wral	|- A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) )
20	2 19	wb	|- ( 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 ) ) )