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

Theorem sotric 5494
 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 5489 . . . . . 6 ((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
2 breq2 5061 . . . . . . 7 (𝐵 = 𝐶 → (𝐵𝑅𝐵𝐵𝑅𝐶))
32notbid 320 . . . . . 6 (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅𝐶))
41, 3syl5ibcom 247 . . . . 5 ((𝑅 Or 𝐴𝐵𝐴) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
54adantrr 715 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
6 so2nr 5492 . . . . . 6 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
7 imnan 402 . . . . . 6 ((𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
86, 7sylibr 236 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵))
98con2d 136 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐶𝑅𝐵 → ¬ 𝐵𝑅𝐶))
105, 9jaod 855 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) → ¬ 𝐵𝑅𝐶))
11 solin 5491 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
12 3orass 1085 . . . . 5 ((𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1311, 12sylib 220 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1413ord 860 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (¬ 𝐵𝑅𝐶 → (𝐵 = 𝐶𝐶𝑅𝐵)))
1510, 14impbid 214 . 2 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) ↔ ¬ 𝐵𝑅𝐶))
1615con2bid 357 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∨ w3o 1081   = wceq 1531   ∈ wcel 2108   class class class wbr 5057   Or wor 5466 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-po 5467  df-so 5468 This theorem is referenced by:  soasym  5497  sotr2  5498  sotri2  5982  sotri3  5983  somin1  5986  somincom  5987  soisores  7072  soisoi  7073  fimaxg  8757  suplub2  8917  supgtoreq  8926  fiming  8954  infsupprpr  8960  ordtypelem7  8980  fpwwe2  10057  indpi  10321  nqereu  10343  ltsonq  10383  prub  10408  ltapr  10459  suplem2pr  10467  ltsosr  10508  axpre-lttri  10579  sotr3  32995  noetalem3  33212  sleloe  33226  prproropf1olem4  43658
 Copyright terms: Public domain W3C validator