Metamath Proof Explorer


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 )