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

Theorem solin 5018
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 4616 . . . . 5 (𝑥 = 𝐵 → (𝑥𝑅𝑦𝐵𝑅𝑦))
2 eqeq1 2625 . . . . 5 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
3 breq2 4617 . . . . 5 (𝑥 = 𝐵 → (𝑦𝑅𝑥𝑦𝑅𝐵))
41, 2, 33orbi123d 1395 . . . 4 (𝑥 = 𝐵 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵)))
54imbi2d 330 . . 3 (𝑥 = 𝐵 → ((𝑅 Or 𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵))))
6 breq2 4617 . . . . 5 (𝑦 = 𝐶 → (𝐵𝑅𝑦𝐵𝑅𝐶))
7 eqeq2 2632 . . . . 5 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
8 breq1 4616 . . . . 5 (𝑦 = 𝐶 → (𝑦𝑅𝐵𝐶𝑅𝐵))
96, 7, 83orbi123d 1395 . . . 4 (𝑦 = 𝐶 → ((𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵) ↔ (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵)))
109imbi2d 330 . . 3 (𝑦 = 𝐶 → ((𝑅 Or 𝐴 → (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))))
11 df-so 4996 . . . . 5 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
12 rsp2 2931 . . . . 5 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
1311, 12simplbiim 658 . . . 4 (𝑅 Or 𝐴 → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
1413com12 32 . . 3 ((𝑥𝐴𝑦𝐴) → (𝑅 Or 𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
155, 10, 14vtocl2ga 3260 . 2 ((𝐵𝐴𝐶𝐴) → (𝑅 Or 𝐴 → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵)))
1615impcom 446 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3o 1035   = wceq 1480  wcel 1987  wral 2907   class class class wbr 4613   Po wpo 4993   Or wor 4994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-so 4996
This theorem is referenced by:  sotric  5021  sotrieq  5022  somo  5029  wecmpep  5066  sorpssi  6896  soxp  7235  wfrlem10  7369  wemaplem2  8396  fpwwe2lem12  9407  fpwwe2lem13  9408  lttri4  10066  xmullem  12037  xmulasslem  12058  orngsqr  29589  socnv  31363  slttri  31533  noreslege  31571  fin2so  33028  fnwe2lem3  37102
  Copyright terms: Public domain W3C validator