# Metamath Proof Explorer

## Theorem sotric

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

Ref Expression
Assertion sotric ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left({B}{R}{C}↔¬\left({B}={C}\vee {C}{R}{B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 sonr ${⊢}\left({R}\mathrm{Or}{A}\wedge {B}\in {A}\right)\to ¬{B}{R}{B}$
2 breq2 ${⊢}{B}={C}\to \left({B}{R}{B}↔{B}{R}{C}\right)$
3 2 notbid ${⊢}{B}={C}\to \left(¬{B}{R}{B}↔¬{B}{R}{C}\right)$
4 1 3 syl5ibcom ${⊢}\left({R}\mathrm{Or}{A}\wedge {B}\in {A}\right)\to \left({B}={C}\to ¬{B}{R}{C}\right)$
5 4 adantrr ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left({B}={C}\to ¬{B}{R}{C}\right)$
6 so2nr ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to ¬\left({B}{R}{C}\wedge {C}{R}{B}\right)$
7 imnan ${⊢}\left({B}{R}{C}\to ¬{C}{R}{B}\right)↔¬\left({B}{R}{C}\wedge {C}{R}{B}\right)$
8 6 7 sylibr ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left({B}{R}{C}\to ¬{C}{R}{B}\right)$
9 8 con2d ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left({C}{R}{B}\to ¬{B}{R}{C}\right)$
10 5 9 jaod ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left(\left({B}={C}\vee {C}{R}{B}\right)\to ¬{B}{R}{C}\right)$
11 solin ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left({B}{R}{C}\vee {B}={C}\vee {C}{R}{B}\right)$
12 3orass ${⊢}\left({B}{R}{C}\vee {B}={C}\vee {C}{R}{B}\right)↔\left({B}{R}{C}\vee \left({B}={C}\vee {C}{R}{B}\right)\right)$
13 11 12 sylib ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left({B}{R}{C}\vee \left({B}={C}\vee {C}{R}{B}\right)\right)$
14 13 ord ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left(¬{B}{R}{C}\to \left({B}={C}\vee {C}{R}{B}\right)\right)$
15 10 14 impbid ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left(\left({B}={C}\vee {C}{R}{B}\right)↔¬{B}{R}{C}\right)$
16 15 con2bid ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({B}\in {A}\wedge {C}\in {A}\right)\right)\to \left({B}{R}{C}↔¬\left({B}={C}\vee {C}{R}{B}\right)\right)$