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

Theorem sotrieq 5623
Description: Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
sotrieq ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵)))

Proof of Theorem sotrieq
StepHypRef Expression
1 sonr 5616 . . . . . . 7 ((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
21adantrr 717 . . . . . 6 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ 𝐵𝑅𝐵)
3 pm1.2 904 . . . . . 6 ((𝐵𝑅𝐵𝐵𝑅𝐵) → 𝐵𝑅𝐵)
42, 3nsyl 140 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐵𝐵𝑅𝐵))
5 breq2 5147 . . . . . . 7 (𝐵 = 𝐶 → (𝐵𝑅𝐵𝐵𝑅𝐶))
6 breq1 5146 . . . . . . 7 (𝐵 = 𝐶 → (𝐵𝑅𝐵𝐶𝑅𝐵))
75, 6orbi12d 919 . . . . . 6 (𝐵 = 𝐶 → ((𝐵𝑅𝐵𝐵𝑅𝐵) ↔ (𝐵𝑅𝐶𝐶𝑅𝐵)))
87notbid 318 . . . . 5 (𝐵 = 𝐶 → (¬ (𝐵𝑅𝐵𝐵𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵)))
94, 8syl5ibcom 245 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵 = 𝐶 → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵)))
109con2d 134 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐵) → ¬ 𝐵 = 𝐶))
11 solin 5619 . . . . . 6 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
12 3orass 1090 . . . . . 6 ((𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
1311, 12sylib 218 . . . . 5 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)))
14 or12 921 . . . . 5 ((𝐵𝑅𝐶 ∨ (𝐵 = 𝐶𝐶𝑅𝐵)) ↔ (𝐵 = 𝐶 ∨ (𝐵𝑅𝐶𝐶𝑅𝐵)))
1513, 14sylib 218 . . . 4 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵 = 𝐶 ∨ (𝐵𝑅𝐶𝐶𝑅𝐵)))
1615ord 865 . . 3 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (¬ 𝐵 = 𝐶 → (𝐵𝑅𝐶𝐶𝑅𝐵)))
1710, 16impbid 212 . 2 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐵) ↔ ¬ 𝐵 = 𝐶))
1817con2bid 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:  sotrieq2  5624  sotrine  5632  sossfld  6206  soisores  7347  soisoi  7348  weniso  7374  soseq  8184  wemapsolem  9590  distrlem4pr  11066  addcanpr  11086  sqgt0sr  11146  lttri2  11343  xrlttri2  13184  xrltne  13205  oneptri  43269
  Copyright terms: Public domain W3C validator