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

Theorem solin 5612
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 2737 . . . . 5 (𝑥 = 𝐵 → (𝑥 = 𝑦𝐵 = 𝑦))
3 breq2 5151 . . . . 5 (𝑥 = 𝐵 → (𝑦𝑅𝑥𝑦𝑅𝐵))
41, 2, 33orbi123d 1436 . . . 4 (𝑥 = 𝐵 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵)))
54imbi2d 341 . . 3 (𝑥 = 𝐵 → ((𝑅 Or 𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵))))
6 breq2 5151 . . . . 5 (𝑦 = 𝐶 → (𝐵𝑅𝑦𝐵𝑅𝐶))
7 eqeq2 2745 . . . . 5 (𝑦 = 𝐶 → (𝐵 = 𝑦𝐵 = 𝐶))
8 breq1 5150 . . . . 5 (𝑦 = 𝐶 → (𝑦𝑅𝐵𝐶𝑅𝐵))
96, 7, 83orbi123d 1436 . . . 4 (𝑦 = 𝐶 → ((𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵) ↔ (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵)))
109imbi2d 341 . . 3 (𝑦 = 𝐶 → ((𝑅 Or 𝐴 → (𝐵𝑅𝑦𝐵 = 𝑦𝑦𝑅𝐵)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))))
11 df-so 5588 . . . . 5 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
12 breq1 5150 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥𝑅𝑦𝑧𝑅𝑦))
13 equequ1 2029 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 = 𝑦𝑧 = 𝑦))
14 breq2 5151 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
1512, 13, 143orbi123d 1436 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝑧𝑅𝑦𝑧 = 𝑦𝑦𝑅𝑧)))
1615ralbidv 3178 . . . . . . . 8 (𝑥 = 𝑧 → (∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑦𝐴 (𝑧𝑅𝑦𝑧 = 𝑦𝑦𝑅𝑧)))
1716rspw 3234 . . . . . . 7 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → (𝑥𝐴 → ∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
18 breq2 5151 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑥𝑅𝑦𝑥𝑅𝑧))
19 equequ2 2030 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑥 = 𝑦𝑥 = 𝑧))
20 breq1 5150 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
2118, 19, 203orbi123d 1436 . . . . . . . 8 (𝑦 = 𝑧 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)))
2221rspw 3234 . . . . . . 7 (∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → (𝑦𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
2317, 22syl6 35 . . . . . 6 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → (𝑥𝐴 → (𝑦𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
2423impd 412 . . . . 5 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
2511, 24simplbiim 506 . . . 4 (𝑅 Or 𝐴 → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
2625com12 32 . . 3 ((𝑥𝐴𝑦𝐴) → (𝑅 Or 𝐴 → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
275, 10, 26vtocl2ga 3566 . 2 ((𝐵𝐴𝐶𝐴) → (𝑅 Or 𝐴 → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵)))
2827impcom 409 1 ((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3o 1087   = wceq 1542  wcel 2107  wral 3062   class class class wbr 5147   Po wpo 5585   Or wor 5586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-so 5588
This theorem is referenced by:  sotric  5615  sotrieq  5616  somo  5624  wecmpep  5667  sorpssi  7714  soxp  8110  wfrlem10OLD  8313  infsupprpr  9495  wemaplem2  9538  fpwwe2lem11  10632  fpwwe2lem12  10633  lttri4  11294  xmullem  13239  xmulasslem  13260  noresle  27180  nosupbnd1lem6  27196  noinfbnd1lem6  27211  sltlin  27232  orngsqr  32391  fin2so  36413  fnwe2lem3  41727  prproropf1olem4  46109
  Copyright terms: Public domain W3C validator