Metamath Proof Explorer

Theorem sotric

Description: A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996)

Ref Expression
Assertion sotric ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ↔ ¬ B = C ∨ C R B

Proof

Step Hyp Ref Expression
1 sonr ⊢ R Or A ∧ B ∈ A → ¬ B R B
2 breq2 ⊢ B = C → B R B ↔ B R C
3 2 notbid ⊢ B = C → ¬ B R B ↔ ¬ B R C
4 1 3 syl5ibcom ⊢ R Or A ∧ B ∈ A → B = C → ¬ B R C
5 4 adantrr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B = C → ¬ B R C
6 so2nr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R C ∧ C R B
7 imnan ⊢ B R C → ¬ C R B ↔ ¬ B R C ∧ C R B
8 6 7 sylibr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C → ¬ C R B
9 8 con2d ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → C R B → ¬ B R C
10 5 9 jaod ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B = C ∨ C R B → ¬ B R C
11 solin ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ∨ B = C ∨ C R B
12 3orass ⊢ B R C ∨ B = C ∨ C R B ↔ B R C ∨ B = C ∨ C R B
13 11 12 sylib ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ∨ B = C ∨ C R B
14 13 ord ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R C → B = C ∨ C R B
15 10 14 impbid ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B = C ∨ C R B ↔ ¬ B R C
16 15 con2bid ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ↔ ¬ B = C ∨ C R B