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 breq1 ⊢ x = z → x R y ↔ z R y
13 equequ1 ⊢ x = z → x = y ↔ z = y
14 breq2 ⊢ x = z → y R x ↔ y R z
15 12 13 14 3orbi123d ⊢ x = z → x R y ∨ x = y ∨ y R x ↔ z R y ∨ z = y ∨ y R z
16 15 ralbidv ⊢ x = z → ∀ y ∈ A x R y ∨ x = y ∨ y R x ↔ ∀ y ∈ A z R y ∨ z = y ∨ y R z
17 16 rspw ⊢ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x → x ∈ A → ∀ y ∈ A x R y ∨ x = y ∨ y R x
18 breq2 ⊢ y = z → x R y ↔ x R z
19 equequ2 ⊢ y = z → x = y ↔ x = z
20 breq1 ⊢ y = z → y R x ↔ z R x
21 18 19 20 3orbi123d ⊢ y = z → x R y ∨ x = y ∨ y R x ↔ x R z ∨ x = z ∨ z R x
22 21 rspw ⊢ ∀ y ∈ A x R y ∨ x = y ∨ y R x → y ∈ A → x R y ∨ x = y ∨ y R x
23 17 22 syl6 ⊢ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x → x ∈ A → y ∈ A → x R y ∨ x = y ∨ y R x
24 23 impd ⊢ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x → x ∈ A ∧ y ∈ A → x R y ∨ x = y ∨ y R x
25 11 24 simplbiim ⊢ R Or A → x ∈ A ∧ y ∈ A → x R y ∨ x = y ∨ y R x
26 25 com12 ⊢ x ∈ A ∧ y ∈ A → R Or A → x R y ∨ x = y ∨ y R x
27 5 10 26 vtocl2ga ⊢ B ∈ A ∧ C ∈ A → R Or A → B R C ∨ B = C ∨ C R B
28 27 impcom ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ∨ B = C ∨ C R B