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

Metamath Proof Explorer

Theorem sotric

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

Ref Expression
Assertion sotric 
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C <-> -. ( B = C \/ C R B ) ) )

Proof

Step Hyp Ref Expression
1 sonr 
 |-  ( ( R Or A /\ B e. A ) -> -. B R B )
2 breq2 
 |-  ( B = C -> ( B R B <-> B R C ) )
3 2 notbid 
 |-  ( B = C -> ( -. B R B <-> -. B R C ) )
4 1 3 syl5ibcom 
 |-  ( ( R Or A /\ B e. A ) -> ( B = C -> -. B R C ) )
5 4 adantrr 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C -> -. B R C ) )
6 so2nr 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )
7 imnan 
 |-  ( ( B R C -> -. C R B ) <-> -. ( B R C /\ C R B ) )
8 6 7 sylibr 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C -> -. C R B ) )
9 8 con2d 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( C R B -> -. B R C ) )
10 5 9 jaod 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B = C \/ C R B ) -> -. B R 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 13 ord 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( -. B R C -> ( B = C \/ C R B ) ) )
15 10 14 impbid 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B = C \/ C R B ) <-> -. B R C ) )
16 15 con2bid 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C <-> -. ( B = C \/ C R B ) ) )