Metamath Proof Explorer

Theorem solin

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

Ref Expression
Assertion solin ⊢ROrA∧B∈A∧C∈A→BRC∨B=C∨CRB

Proof

Step Hyp Ref Expression
1 breq1 ⊢x=B→xRy↔BRy
2 eqeq1 ⊢x=B→x=y↔B=y
3 breq2 ⊢x=B→yRx↔yRB
4 1 2 3 3orbi123d ⊢x=B→xRy∨x=y∨yRx↔BRy∨B=y∨yRB
5 4 imbi2d ⊢x=B→ROrA→xRy∨x=y∨yRx↔ROrA→BRy∨B=y∨yRB
6 breq2 ⊢y=C→BRy↔BRC
7 eqeq2 ⊢y=C→B=y↔B=C
8 breq1 ⊢y=C→yRB↔CRB
9 6 7 8 3orbi123d ⊢y=C→BRy∨B=y∨yRB↔BRC∨B=C∨CRB
10 9 imbi2d ⊢y=C→ROrA→BRy∨B=y∨yRB↔ROrA→BRC∨B=C∨CRB
11 df-so ⊢ROrA↔RPoA∧∀x∈A∀y∈AxRy∨x=y∨yRx
12 breq1 ⊢x=z→xRy↔zRy
13 equequ1 ⊢x=z→x=y↔z=y
14 breq2 ⊢x=z→yRx↔yRz
15 12 13 14 3orbi123d ⊢x=z→xRy∨x=y∨yRx↔zRy∨z=y∨yRz
16 15 ralbidv ⊢x=z→∀y∈AxRy∨x=y∨yRx↔∀y∈AzRy∨z=y∨yRz
17 16 rspw ⊢∀x∈A∀y∈AxRy∨x=y∨yRx→x∈A→∀y∈AxRy∨x=y∨yRx
18 breq2 ⊢y=z→xRy↔xRz
19 equequ2 ⊢y=z→x=y↔x=z
20 breq1 ⊢y=z→yRx↔zRx
21 18 19 20 3orbi123d ⊢y=z→xRy∨x=y∨yRx↔xRz∨x=z∨zRx
22 21 rspw ⊢∀y∈AxRy∨x=y∨yRx→y∈A→xRy∨x=y∨yRx
23 17 22 syl6 ⊢∀x∈A∀y∈AxRy∨x=y∨yRx→x∈A→y∈A→xRy∨x=y∨yRx
24 23 impd ⊢∀x∈A∀y∈AxRy∨x=y∨yRx→x∈A∧y∈A→xRy∨x=y∨yRx
25 11 24 simplbiim ⊢ROrA→x∈A∧y∈A→xRy∨x=y∨yRx
26 25 com12 ⊢x∈A∧y∈A→ROrA→xRy∨x=y∨yRx
27 5 10 26 vtocl2ga ⊢B∈A∧C∈A→ROrA→BRC∨B=C∨CRB
28 27 impcom ⊢ROrA∧B∈A∧C∈A→BRC∨B=C∨CRB