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

Theorem sotric 4832
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 4827 . . . . . 6  |-  ( ( R  Or  A  /\  B  e.  A )  ->  -.  B R B )
2 breq2 4457 . . . . . . 7  |-  ( B  =  C  ->  ( B R B  <->  B R C ) )
32notbid 294 . . . . . 6  |-  ( B  =  C  ->  ( -.  B R B  <->  -.  B R C ) )
41, 3syl5ibcom 220 . . . . 5  |-  ( ( R  Or  A  /\  B  e.  A )  ->  ( B  =  C  ->  -.  B R C ) )
54adantrr 716 . . . 4  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B  =  C  ->  -.  B R C ) )
6 so2nr 4830 . . . . . 6  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  -.  ( B R C  /\  C R B ) )
7 imnan 422 . . . . . 6  |-  ( ( B R C  ->  -.  C R B )  <->  -.  ( B R C  /\  C R B ) )
86, 7sylibr 212 . . . . 5  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B R C  ->  -.  C R B ) )
98con2d 115 . . . 4  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( C R B  ->  -.  B R C ) )
105, 9jaod 380 . . 3  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  (
( B  =  C  \/  C R B )  ->  -.  B R C ) )
11 solin 4829 . . . 4  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B R C  \/  B  =  C  \/  C R B ) )
12 3orass 976 . . . . 5  |-  ( ( B R C  \/  B  =  C  \/  C R B )  <->  ( B R C  \/  ( B  =  C  \/  C R B ) ) )
13 df-or 370 . . . . 5  |-  ( ( B R C  \/  ( B  =  C  \/  C R B ) )  <->  ( -.  B R C  ->  ( B  =  C  \/  C R B ) ) )
1412, 13bitri 249 . . . 4  |-  ( ( B R C  \/  B  =  C  \/  C R B )  <->  ( -.  B R C  ->  ( B  =  C  \/  C R B ) ) )
1511, 14sylib 196 . . 3  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( -.  B R C  -> 
( B  =  C  \/  C R B ) ) )
1610, 15impbid 191 . 2  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  (
( B  =  C  \/  C R B )  <->  -.  B R C ) )
1716con2bid 329 1  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B R C  <->  -.  ( B  =  C  \/  C R B ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    \/ w3o 972    = wceq 1379    e. wcel 1767   class class class wbr 4453    Or wor 4805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-br 4454  df-po 4806  df-so 4807
This theorem is referenced by:  sotr2  4835  sotri2  5402  sotri3  5403  somin1  5409  somincom  5410  soisores  6222  soisoi  6223  fimaxg  7779  suplub2  7933  supgtoreq  7940  ordtypelem7  7961  fpwwe2  9033  indpi  9297  nqereu  9319  ltsonq  9359  prub  9384  ltapr  9435  suplem2pr  9443  ltsosr  9483  axpre-lttri  9554
  Copyright terms: Public domain W3C validator