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

Theorem soasym 5628
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 5625 . 2 ((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴)) → (𝑋𝑅𝑌 ↔ ¬ (𝑋 = 𝑌𝑌𝑅𝑋)))
2 pm2.46 882 . 2 (¬ (𝑋 = 𝑌𝑌𝑅𝑋) → ¬ 𝑌𝑅𝑋)
31, 2biimtrdi 253 1 ((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847   = wceq 1536  wcel 2105   class class class wbr 5147   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-po 5596  df-so 5597
This theorem is referenced by:  fiinfg  9536  noresle  27756  nosupprefixmo  27759  noinfprefixmo  27760  nosupbnd1lem1  27767  nosupbnd1lem4  27770  nosupbnd2lem1  27774  nosupbnd2  27775  noinfbnd1lem1  27782  noinfbnd1lem4  27785  noinfbnd2lem1  27789  noinfbnd2  27790  sltasym  27807  or2expropbi  46983  prproropf1olem3  47429
  Copyright terms: Public domain W3C validator