This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. A /\ C e. A ) ) -> ( B = C <-> -. ( B R C \/ C R B ) ) )

Proof

Step Hyp Ref Expression
1 sonr 
 |-  ( ( R Or A /\ B e. A ) -> -. B R B )
2 1 adantrr 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> -. B R B )
3 pm1.2 
 |-  ( ( B R B \/ B R B ) -> B R B )
4 2 3 nsyl 
 |-  ( ( R Or A /\ ( B e. A /\ C e. 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 e. A /\ C e. A ) ) -> ( B = C -> -. ( B R C \/ C R B ) ) )
10 9 con2d 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B R C \/ C R B ) -> -. B = C ) )
11 solin 
 |-  ( ( R Or A /\ ( B e. A /\ C e. 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 e. A /\ C e. 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 e. A /\ C e. A ) ) -> ( B = C \/ ( B R C \/ C R B ) ) )
16 15 ord 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( -. B = C -> ( B R C \/ C R B ) ) )
17 10 16 impbid 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B R C \/ C R B ) <-> -. B = C ) )
18 17 con2bid 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C <-> -. ( B R C \/ C R B ) ) )