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

Theorem solin 5087
 Description: A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.)
Assertion
Ref Expression
solin ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))

Proof of Theorem solin
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 4688 . . . . 5 (𝑥 = 𝐵 → (𝑥𝑅𝑦𝐵𝑅𝑦))
2 eqeq1 2655 . . . . 5 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
3 breq2 4689 . . . . 5 (𝑥 = 𝐵 → (𝑦𝑅𝑥𝑦𝑅𝐵))
41, 2, 33orbi123d 1438 . . . 4 (𝑥 = 𝐵 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵)))
54imbi2d 329 . . 3 (𝑥 = 𝐵 → ((𝑅 Or 𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵))))
6 breq2 4689 . . . . 5 (𝑦 = 𝐶 → (𝐵𝑅𝑦𝐵𝑅𝐶))
7 eqeq2 2662 . . . . 5 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
8 breq1 4688 . . . . 5 (𝑦 = 𝐶 → (𝑦𝑅𝐵𝐶𝑅𝐵))
96, 7, 83orbi123d 1438 . . . 4 (𝑦 = 𝐶 → ((𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵) ↔ (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵)))
109imbi2d 329 . . 3 (𝑦 = 𝐶 → ((𝑅 Or 𝐴 → (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))))
11 df-so 5065 . . . . 5 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
12 rsp2 2965 . . . . 5 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
1311, 12simplbiim 659 . . . 4 (𝑅 Or 𝐴 → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
1413com12 32 . . 3 ((𝑥𝐴𝑦𝐴) → (𝑅 Or 𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
155, 10, 14vtocl2ga 3305 . 2 ((𝐵𝐴𝐶𝐴) → (𝑅 Or 𝐴 → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵)))
1615impcom 445 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∨ w3o 1053   = wceq 1523   ∈ wcel 2030  ∀wral 2941   class class class wbr 4685   Po wpo 5062   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-so 5065 This theorem is referenced by:  sotric  5090  sotrieq  5091  somo  5098  wecmpep  5135  sorpssi  6985  soxp  7335  wfrlem10  7469  wemaplem2  8493  fpwwe2lem12  9501  fpwwe2lem13  9502  lttri4  10160  xmullem  12132  xmulasslem  12153  orngsqr  29932  noresle  31971  nosupbnd1lem6  31984  sltlin  31999  fin2so  33526  fnwe2lem3  37939
 Copyright terms: Public domain W3C validator