Theorem issod

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	issod.1	|- ( ph -> R Po A )
	issod.2	|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x R y \/ x = y \/ y R x ) )
Assertion	issod	|- ( ph -> R Or A )

Proof

Step	Hyp	Ref	Expression
1		issod.1	|- ( ph -> R Po A )
2		issod.2	|- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x R y \/ x = y \/ y R x ) )
3	2	ralrimivva	|- ( ph -> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) )
4		df-so	|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
5	1 3 4	sylanbrc	|- ( ph -> R Or A )