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

Theorem sotric 4975
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 4970 . . . . . 6 ((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
2 breq2 4581 . . . . . . 7 (𝐵 = 𝐶 → (𝐵𝑅𝐵𝐵𝑅𝐶))
32notbid 306 . . . . . 6 (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅𝐶))
41, 3syl5ibcom 233 . . . . 5 ((𝑅 Or 𝐴𝐵𝐴) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
54adantrr 748 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
6 so2nr 4973 . . . . . 6 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
7 imnan 436 . . . . . 6 ((𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
86, 7sylibr 222 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵))
98con2d 127 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐶𝑅𝐵 → ¬ 𝐵𝑅𝐶))
105, 9jaod 393 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) → ¬ 𝐵𝑅𝐶))
11 solin 4972 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
12 3orass 1033 . . . . 5 ((𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1311, 12sylib 206 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1413ord 390 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (¬ 𝐵𝑅𝐶 → (𝐵 = 𝐶𝐶𝑅𝐵)))
1510, 14impbid 200 . 2 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) ↔ ¬ 𝐵𝑅𝐶))
1615con2bid 342 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3o 1029   = wceq 1474  wcel 1976   class class class wbr 4577   Or wor 4948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-po 4949  df-so 4950
This theorem is referenced by:  sotr2  4978  sotri2  5431  sotri3  5432  somin1  5435  somincom  5436  soisores  6455  soisoi  6456  fimaxg  8069  suplub2  8227  supgtoreq  8236  fiming  8264  ordtypelem7  8289  fpwwe2  9321  indpi  9585  nqereu  9607  ltsonq  9647  prub  9672  ltapr  9723  suplem2pr  9731  ltsosr  9771  axpre-lttri  9842
  Copyright terms: Public domain W3C validator