MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sotric Unicode version

Theorem sotric 4340
Description: A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.)
Assertion
Ref Expression
sotric  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B R C  <->  -.  ( B  =  C  \/  C R B ) ) )

Proof of Theorem sotric
StepHypRef Expression
1 sonr 4335 . . . . . 6  |-  ( ( R  Or  A  /\  B  e.  A )  ->  -.  B R B )
2 breq2 4027 . . . . . . 7  |-  ( B  =  C  ->  ( B R B  <->  B R C ) )
32notbid 285 . . . . . 6  |-  ( B  =  C  ->  ( -.  B R B  <->  -.  B R C ) )
41, 3syl5ibcom 211 . . . . 5  |-  ( ( R  Or  A  /\  B  e.  A )  ->  ( B  =  C  ->  -.  B R C ) )
54adantrr 697 . . . 4  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B  =  C  ->  -.  B R C ) )
6 so2nr 4338 . . . . . 6  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  -.  ( B R C  /\  C R B ) )
7 imnan 411 . . . . . 6  |-  ( ( B R C  ->  -.  C R B )  <->  -.  ( B R C  /\  C R B ) )
86, 7sylibr 203 . . . . 5  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B R C  ->  -.  C R B ) )
98con2d 107 . . . 4  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( C R B  ->  -.  B R C ) )
105, 9jaod 369 . . 3  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  (
( B  =  C  \/  C R B )  ->  -.  B R C ) )
11 solin 4337 . . . 4  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B R C  \/  B  =  C  \/  C R B ) )
12 3orass 937 . . . . 5  |-  ( ( B R C  \/  B  =  C  \/  C R B )  <->  ( B R C  \/  ( B  =  C  \/  C R B ) ) )
13 df-or 359 . . . . 5  |-  ( ( B R C  \/  ( B  =  C  \/  C R B ) )  <->  ( -.  B R C  ->  ( B  =  C  \/  C R B ) ) )
1412, 13bitri 240 . . . 4  |-  ( ( B R C  \/  B  =  C  \/  C R B )  <->  ( -.  B R C  ->  ( B  =  C  \/  C R B ) ) )
1511, 14sylib 188 . . 3  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( -.  B R C  -> 
( B  =  C  \/  C R B ) ) )
1610, 15impbid 183 . 2  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  (
( B  =  C  \/  C R B )  <->  -.  B R C ) )
1716con2bid 319 1  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B R C  <->  -.  ( B  =  C  \/  C R B ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 933    = wceq 1623    e. wcel 1684   class class class wbr 4023    Or wor 4313
This theorem is referenced by:  sotr2  4343  sotri2  5072  sotri3  5073  somin1  5079  somincom  5080  soisores  5824  soisoi  5825  fimaxg  7104  suplub2  7212  ordtypelem7  7239  fpwwe2  8265  indpi  8531  nqereu  8553  ltsonq  8593  prub  8618  ltapr  8669  suplem2pr  8677  ltsosr  8716  axpre-lttri  8787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-po 4314  df-so 4315
  Copyright terms: Public domain W3C validator