Metamath Proof Explorer

Theorem sotrieq

Description: Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 sonr ⊢ R Or A ∧ B ∈ A → ¬ B R B
2 1 adantrr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R B
3 pm1.2 ⊢ B R B ∨ B R B → B R B
4 2 3 nsyl ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R B ∨ B R B
5 breq2 ⊢ B = C → B R B ↔ B R C
6 breq1 ⊢ B = C → B R B ↔ C R B
7 5 6 orbi12d ⊢ B = C → B R B ∨ B R B ↔ B R C ∨ C R B
8 7 notbid ⊢ B = C → ¬ B R B ∨ B R B ↔ ¬ B R C ∨ C R B
9 4 8 syl5ibcom ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B = C → ¬ B R C ∨ C R B
10 9 con2d ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ∨ C R B → ¬ B = 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 or12 ⊢ B R C ∨ B = C ∨ C R B ↔ B = C ∨ B R C ∨ C R B
15 13 14 sylib ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B = C ∨ B R C ∨ C R B
16 15 ord ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B = C → B R C ∨ C R B
17 10 16 impbid ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ∨ C R B ↔ ¬ B = C
18 17 con2bid ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B = C ↔ ¬ B R C ∨ C R B