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

Theorem solin 5622
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 5150 . . . . 5 (𝑥 = 𝐵 → (𝑥𝑅𝑦𝐵𝑅𝑦))
2 eqeq1 2738 . . . . 5 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
3 breq2 5151 . . . . 5 (𝑥 = 𝐵 → (𝑦𝑅𝑥𝑦𝑅𝐵))
41, 2, 33orbi123d 1434 . . . 4 (𝑥 = 𝐵 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵)))
54imbi2d 340 . . 3 (𝑥 = 𝐵 → ((𝑅 Or 𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵))))
6 breq2 5151 . . . . 5 (𝑦 = 𝐶 → (𝐵𝑅𝑦𝐵𝑅𝐶))
7 eqeq2 2746 . . . . 5 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
8 breq1 5150 . . . . 5 (𝑦 = 𝐶 → (𝑦𝑅𝐵𝐶𝑅𝐵))
96, 7, 83orbi123d 1434 . . . 4 (𝑦 = 𝐶 → ((𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵) ↔ (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵)))
109imbi2d 340 . . 3 (𝑦 = 𝐶 → ((𝑅 Or 𝐴 → (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))))
11 df-so 5597 . . . . 5 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
12 breq1 5150 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥𝑅𝑦𝑧𝑅𝑦))
13 equequ1 2021 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
14 breq2 5151 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
1512, 13, 143orbi123d 1434 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝑧𝑅𝑦𝑧 = 𝑦𝑦𝑅𝑧)))
1615ralbidv 3175 . . . . . . . 8 (𝑥 = 𝑧 → (∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑦𝐴 (𝑧𝑅𝑦𝑧 = 𝑦𝑦𝑅𝑧)))
1716rspw 3233 . . . . . . 7 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → (𝑥𝐴 → ∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
18 breq2 5151 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑥𝑅𝑦𝑥𝑅𝑧))
19 equequ2 2022 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑥 = 𝑦𝑥 = 𝑧))
20 breq1 5150 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
2118, 19, 203orbi123d 1434 . . . . . . . 8 (𝑦 = 𝑧 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)))
2221rspw 3233 . . . . . . 7 (∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → (𝑦𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
2317, 22syl6 35 . . . . . 6 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → (𝑥𝐴 → (𝑦𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
2423impd 410 . . . . 5 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
2511, 24simplbiim 504 . . . 4 (𝑅 Or 𝐴 → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
2625com12 32 . . 3 ((𝑥𝐴𝑦𝐴) → (𝑅 Or 𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
275, 10, 26vtocl2ga 3577 . 2 ((𝐵𝐴𝐶𝐴) → (𝑅 Or 𝐴 → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵)))
2827impcom 407 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3o 1085   = wceq 1536  wcel 2105  wral 3058   class class class wbr 5147   Po wpo 5594   Or wor 5595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-so 5597
This theorem is referenced by:  sotric  5625  sotrieq  5626  somo  5634  wecmpep  5680  sorpssi  7747  soxp  8152  wfrlem10OLD  8356  infsupprpr  9541  wemaplem2  9584  fpwwe2lem11  10678  fpwwe2lem12  10679  lttri4  11342  xmullem  13302  xmulasslem  13323  noresle  27756  nosupbnd1lem6  27772  noinfbnd1lem6  27787  sltlin  27808  orngsqr  33313  weiunso  36448  fin2so  37593  fnwe2lem3  43040  prproropf1olem4  47430
  Copyright terms: Public domain W3C validator