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

Theorem sotric 5090
 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 5085 . . . . . 6 ((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
2 breq2 4689 . . . . . . 7 (𝐵 = 𝐶 → (𝐵𝑅𝐵𝐵𝑅𝐶))
32notbid 307 . . . . . 6 (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅𝐶))
41, 3syl5ibcom 235 . . . . 5 ((𝑅 Or 𝐴𝐵𝐴) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
54adantrr 753 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
6 so2nr 5088 . . . . . 6 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
7 imnan 437 . . . . . 6 ((𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
86, 7sylibr 224 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵))
98con2d 129 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐶𝑅𝐵 → ¬ 𝐵𝑅𝐶))
105, 9jaod 394 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) → ¬ 𝐵𝑅𝐶))
11 solin 5087 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
12 3orass 1057 . . . . 5 ((𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1311, 12sylib 208 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1413ord 391 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (¬ 𝐵𝑅𝐶 → (𝐵 = 𝐶𝐶𝑅𝐵)))
1510, 14impbid 202 . 2 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵 = 𝐶𝐶𝑅𝐵) ↔ ¬ 𝐵𝑅𝐶))
1615con2bid 343 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∨ w3o 1053   = wceq 1523   ∈ wcel 2030   class class class wbr 4685   Or wor 5063 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-po 5064  df-so 5065 This theorem is referenced by:  sotr2  5093  sotri2  5560  sotri3  5561  somin1  5564  somincom  5565  soisores  6617  soisoi  6618  fimaxg  8248  suplub2  8408  supgtoreq  8417  fiming  8445  ordtypelem7  8470  fpwwe2  9503  indpi  9767  nqereu  9789  ltsonq  9829  prub  9854  ltapr  9905  suplem2pr  9913  ltsosr  9953  axpre-lttri  10024  sotr3  31782  soasym  31783  noetalem3  31990  sleloe  32004
 Copyright terms: Public domain W3C validator