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 A ¬ x R x
issoi.2 x A y A z A x R y y R z x R z
issoi.3 x A y A x R y x = y y R x
Assertion issoi R Or A

Proof

Step Hyp Ref Expression
1 issoi.1 x A ¬ x R x
2 issoi.2 x A y A z A x R y y R z x R z
3 issoi.3 x A y A x R y x = y y R x
4 1 adantl x A ¬ x R x
5 2 adantl x A y A z A x R y y R z x R z
6 4 5 ispod R Po A
7 3 adantl x A y A x R y x = y y R x
8 6 7 issod R Or A
9 8 mptru R Or A