Metamath Proof Explorer

Theorem sotrine

Description: Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion sotrine ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B ≠ C ↔ B R C ∨ C R B

Proof

Step Hyp Ref Expression
1 sotrieq ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B = C ↔ ¬ B R C ∨ C R B
2 1 bicomd ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R C ∨ C R B ↔ B = C
3 2 necon1abid ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B ≠ C ↔ B R C ∨ C R B