This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )