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

Theorem soasym 5473
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 5470 . 2 ((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴)) → (𝑋𝑅𝑌 ↔ ¬ (𝑋 = 𝑌𝑌𝑅𝑋)))
2 pm2.46 882 . 2 (¬ (𝑋 = 𝑌𝑌𝑅𝑋) → ¬ 𝑌𝑅𝑋)
31, 2syl6bi 256 1 ((𝑅 Or 𝐴 ∧ (𝑋𝐴𝑌𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 846   = wceq 1542  wcel 2114   class class class wbr 5030   Or wor 5441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-v 3400  df-un 3848  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-po 5442  df-so 5443
This theorem is referenced by:  fiinfg  9036  noresle  33543  nosupprefixmo  33546  noinfprefixmo  33547  nosupbnd1lem1  33554  nosupbnd1lem4  33557  nosupbnd2lem1  33561  nosupbnd2  33562  noinfbnd1lem1  33569  noinfbnd1lem4  33572  noinfbnd2lem1  33576  noinfbnd2  33577  sltasym  33594  or2expropbi  44087  prproropf1olem3  44511
  Copyright terms: Public domain W3C validator