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 ( 𝜑𝑅 Po 𝐴 )
issod.2 ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) )
Assertion issod ( 𝜑𝑅 Or 𝐴 )

Proof

Step Hyp Ref Expression
1 issod.1 ( 𝜑𝑅 Po 𝐴 )
2 issod.2 ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) )
3 2 ralrimivva ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) )
4 df-so ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
5 1 3 4 sylanbrc ( 𝜑𝑅 Or 𝐴 )