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

Metamath Proof Explorer

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 )