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