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

Theorem sotric 5622
Description: A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.)
Assertion
Ref Expression
sotric ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))

Proof of Theorem sotric
StepHypRef Expression
1 sonr 5616 . . . . . 6 ((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
2 breq2 5147 . . . . . . 7 (𝐵 = 𝐶 → (𝐵𝑅𝐵𝐵𝑅𝐶))
32notbid 318 . . . . . 6 (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅𝐶))
41, 3syl5ibcom 245 . . . . 5 ((𝑅 Or 𝐴𝐵𝐴) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
54adantrr 717 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
6 so2nr 5620 . . . . . 6 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
7 imnan 399 . . . . . 6 ((𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
86, 7sylibr 234 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵))
98con2d 134 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐶𝑅𝐵 → ¬ 𝐵𝑅𝐶))
105, 9jaod 860 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) → ¬ 𝐵𝑅𝐶))
11 solin 5619 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
12 3orass 1090 . . . . 5 ((𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1311, 12sylib 218 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1413ord 865 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (¬ 𝐵𝑅𝐶 → (𝐵 = 𝐶𝐶𝑅𝐵)))
1510, 14impbid 212 . 2 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) ↔ ¬ 𝐵𝑅𝐶))
1615con2bid 354 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3o 1086   = wceq 1540  wcel 2108   class class class wbr 5143   Or wor 5591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-po 5592  df-so 5593
This theorem is referenced by:  soasym  5625  sotr2  5626  sotr3  5633  sotri2  6149  sotri3  6150  somin1  6153  somincom  6154  soisores  7347  soisoi  7348  fimaxg  9323  suplub2  9501  supgtoreq  9510  fiming  9538  infsupprpr  9544  ordtypelem7  9564  fpwwe2  10683  indpi  10947  nqereu  10969  ltsonq  11009  prub  11034  ltapr  11085  suplem2pr  11093  ltsosr  11134  axpre-lttri  11205  noetasuplem4  27781  noetainflem4  27785  sleloe  27799  prproropf1olem4  47493
  Copyright terms: Public domain W3C validator