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

Metamath Proof Explorer

Theorem issoi

Description: An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996) (Revised by Mario Carneiro, 9-Jul-2014)

Ref Expression
Hypotheses issoi.1 
|- ( x e. A -> -. x R x )
issoi.2 
|- ( ( x e. A /\ y e. A /\ z e. A ) -> ( ( x R y /\ y R z ) -> x R z ) )
issoi.3 
|- ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) )
Assertion issoi 
|- R Or A

Proof

Step Hyp Ref Expression
1 issoi.1 
 |-  ( x e. A -> -. x R x )
2 issoi.2 
 |-  ( ( x e. A /\ y e. A /\ z e. A ) -> ( ( x R y /\ y R z ) -> x R z ) )
3 issoi.3 
 |-  ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) )
4 1 adantl 
 |-  ( ( T. /\ x e. A ) -> -. x R x )
5 2 adantl 
 |-  ( ( T. /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R y /\ y R z ) -> x R z ) )
6 4 5 ispod 
 |-  ( T. -> R Po A )
7 3 adantl 
 |-  ( ( T. /\ ( x e. A /\ y e. A ) ) -> ( x R y \/ x = y \/ y R x ) )
8 6 7 issod 
 |-  ( T. -> R Or A )
9 8 mptru 
 |-  R Or A