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

Theorem sotric 5617
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 5612 . . . . . 6 ((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
2 breq2 5153 . . . . . . 7 (𝐵 = 𝐶 → (𝐵𝑅𝐵𝐵𝑅𝐶))
32notbid 317 . . . . . 6 (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅𝐶))
41, 3syl5ibcom 244 . . . . 5 ((𝑅 Or 𝐴𝐵𝐴) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
54adantrr 713 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
6 so2nr 5615 . . . . . 6 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
7 imnan 398 . . . . . 6 ((𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
86, 7sylibr 233 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵))
98con2d 134 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐶𝑅𝐵 → ¬ 𝐵𝑅𝐶))
105, 9jaod 855 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) → ¬ 𝐵𝑅𝐶))
11 solin 5614 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
12 3orass 1088 . . . . 5 ((𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1311, 12sylib 217 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1413ord 860 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (¬ 𝐵𝑅𝐶 → (𝐵 = 𝐶𝐶𝑅𝐵)))
1510, 14impbid 211 . 2 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) ↔ ¬ 𝐵𝑅𝐶))
1615con2bid 353 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 843  w3o 1084   = wceq 1539  wcel 2104   class class class wbr 5149   Or wor 5588
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-po 5589  df-so 5590
This theorem is referenced by:  soasym  5620  sotr2  5621  sotr3  5628  sotri2  6131  sotri3  6132  somin1  6135  somincom  6136  soisores  7328  soisoi  7329  fimaxg  9294  suplub2  9460  supgtoreq  9469  fiming  9497  infsupprpr  9503  ordtypelem7  9523  fpwwe2  10642  indpi  10906  nqereu  10928  ltsonq  10968  prub  10993  ltapr  11044  suplem2pr  11052  ltsosr  11093  axpre-lttri  11164  noetasuplem4  27473  noetainflem4  27477  sleloe  27491  prproropf1olem4  46474
  Copyright terms: Public domain W3C validator