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

Theorem soasym 5620
Description: Asymmetry law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.)
Assertion
Ref Expression
soasym ((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋))

Proof of Theorem soasym
StepHypRef Expression
1 sotric 5617 . 2 ((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴)) → (𝑋𝑅𝑌 ↔ ¬ (𝑋 = 𝑌𝑌𝑅𝑋)))
2 pm2.46 882 . 2 (¬ (𝑋 = 𝑌𝑌𝑅𝑋) → ¬ 𝑌𝑅𝑋)
31, 2syl6bi 253 1 ((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wo 846   = wceq 1542  wcel 2107   class class class wbr 5149   Or wor 5588
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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-po 5589  df-so 5590
This theorem is referenced by:  fiinfg  9494  noresle  27200  nosupprefixmo  27203  noinfprefixmo  27204  nosupbnd1lem1  27211  nosupbnd1lem4  27214  nosupbnd2lem1  27218  nosupbnd2  27219  noinfbnd1lem1  27226  noinfbnd1lem4  27229  noinfbnd2lem1  27233  noinfbnd2  27234  sltasym  27251  or2expropbi  45744  prproropf1olem3  46173
  Copyright terms: Public domain W3C validator