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

Theorem solin 4664
Description: A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.)
Assertion
Ref Expression
solin  |-  ( ( R  Or  A  /\  ( B  e.  A  /\  C  e.  A
) )  ->  ( B R C  \/  B  =  C  \/  C R B ) )

Proof of Theorem solin
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 4295 . . . . 5  |-  ( x  =  B  ->  (
x R y  <->  B R
y ) )
2 eqeq1 2449 . . . . 5  |-  ( x  =  B  ->  (
x  =  y  <->  B  =  y ) )
3 breq2 4296 . . . . 5  |-  ( x  =  B  ->  (
y R x  <->  y R B ) )
41, 2, 33orbi123d 1288 . . . 4  |-  ( x  =  B  ->  (
( x R y  \/  x  =  y  \/  y R x )  <->  ( B R y  \/  B  =  y  \/  y R B ) ) )
54imbi2d 316 . . 3  |-  ( x  =  B  ->  (
( R  Or  A  ->  ( x R y  \/  x  =  y  \/  y R x ) )  <->  ( R  Or  A  ->  ( B R y  \/  B  =  y  \/  y R B ) ) ) )
6 breq2 4296 . . . . 5  |-  ( y  =  C  ->  ( B R y  <->  B R C ) )
7 eqeq2 2452 . . . . 5  |-  ( y  =  C  ->  ( B  =  y  <->  B  =  C ) )
8 breq1 4295 . . . . 5  |-  ( y  =  C  ->  (
y R B  <->  C R B ) )
96, 7, 83orbi123d 1288 . . . 4  |-  ( y  =  C  ->  (
( B R y  \/  B  =  y  \/  y R B )  <->  ( B R C  \/  B  =  C  \/  C R B ) ) )
109imbi2d 316 . . 3  |-  ( y  =  C  ->  (
( R  Or  A  ->  ( B R y  \/  B  =  y  \/  y R B ) )  <->  ( R  Or  A  ->  ( B R C  \/  B  =  C  \/  C R B ) ) ) )
11 df-so 4642 . . . . 5  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
12 rsp2 2778 . . . . . 6  |-  ( A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x )  ->  ( ( x  e.  A  /\  y  e.  A )  ->  (
x R y  \/  x  =  y  \/  y R x ) ) )
1312adantl 466 . . . . 5  |-  ( ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) )  ->  ( (
x  e.  A  /\  y  e.  A )  ->  ( x R y  \/  x  =  y  \/  y R x ) ) )
1411, 13sylbi 195 . . . 4  |-  ( R  Or  A  ->  (
( x  e.  A  /\  y  e.  A
)  ->  ( x R y  \/  x  =  y  \/  y R x ) ) )
1514com12 31 . . 3  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ( R  Or  A  ->  ( x R y  \/  x  =  y  \/  y R x ) ) )
165, 10, 15vtocl2ga 3038 . 2  |-  ( ( B  e.  A  /\  C  e.  A )  ->  ( R  Or  A  ->  ( B R C  \/  B  =  C  \/  C R B ) ) )
1716impcom 430 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:    -> wi 4    /\ wa 369    \/ w3o 964    = wceq 1369    e. wcel 1756   A.wral 2715   class class class wbr 4292    Po wpo 4639    Or wor 4640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-so 4642
This theorem is referenced by:  sotric  4667  sotrieq  4668  somo  4675  wecmpep  4712  sorpssi  6366  soxp  6685  wemaplem2  7761  fpwwe2lem12  8808  fpwwe2lem13  8809  lttri4  9459  xmullem  11227  xmulasslem  11248  orngsqr  26272  socnv  27575  wfrlem10  27733  slttri  27814  fin2so  28416  fnwe2lem3  29405
  Copyright terms: Public domain W3C validator