Theorem ispod

Description: Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014)

	Ref	Expression
Hypotheses	ispod.1	|- ( ( ph /\ x e. A ) -> -. x R x )
	ispod.2	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R y /\ y R z ) -> x R z ) )
Assertion	ispod	|- ( ph -> R Po A )

Proof

Step	Hyp	Ref	Expression
1		ispod.1	|- ( ( ph /\ x e. A ) -> -. x R x )
2		ispod.2	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R y /\ y R z ) -> x R z ) )
3	1	3ad2antr1	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. x R x )
4	3 2	jca	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
5	4	ralrimivvva	|- ( ph -> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
6		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 ) ) )
7	5 6	sylibr	|- ( ph -> R Po A )