Metamath Proof Explorer

Theorem solin

Description: A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996)

Ref Expression
Assertion solin ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ∨ B = C ∨ C R B

Proof

Step Hyp Ref Expression
1 breq1 ⊢ x = B → x R y ↔ B R y
2 eqeq1 ⊢ x = B → x = y ↔ B = y
3 breq2 ⊢ x = B → y R x ↔ y R B
4 1 2 3 3orbi123d ⊢ x = B → x R y ∨ x = y ∨ y R x ↔ B R y ∨ B = y ∨ y R B
5 4 imbi2d ⊢ x = B → R Or A → x R y ∨ x = y ∨ y R x ↔ R Or A → B R y ∨ B = y ∨ y R B
6 breq2 ⊢ y = C → B R y ↔ B R C
7 eqeq2 ⊢ y = C → B = y ↔ B = C
8 breq1 ⊢ y = C → y R B ↔ C R B
9 6 7 8 3orbi123d ⊢ y = C → B R y ∨ B = y ∨ y R B ↔ B R C ∨ B = C ∨ C R B
10 9 imbi2d ⊢ y = C → R Or A → B R y ∨ B = y ∨ y R B ↔ R Or A → B R C ∨ B = C ∨ C R B
11 df-so ⊢ R Or A ↔ R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
12 rsp2 ⊢ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x → x ∈ A ∧ y ∈ A → x R y ∨ x = y ∨ y R x
13 11 12 simplbiim ⊢ R Or A → x ∈ A ∧ y ∈ A → x R y ∨ x = y ∨ y R x
14 13 com12 ⊢ x ∈ A ∧ y ∈ A → R Or A → x R y ∨ x = y ∨ y R x
15 5 10 14 vtocl2ga ⊢ B ∈ A ∧ C ∈ A → R Or A → B R C ∨ B = C ∨ C R B
16 15 impcom ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ∨ B = C ∨ C R B