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

Theorem sonr 5569
Description: A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
Assertion
Ref Expression
sonr ((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)

Proof of Theorem sonr
StepHypRef Expression
1 sopo 5565 . 2 (𝑅 Or 𝐴𝑅 Po 𝐴)
2 poirr 5558 . 2 ((𝑅 Po 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
31, 2sylan 581 1 ((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wcel 2107   class class class wbr 5106   Po wpo 5544   Or wor 5545
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-po 5546  df-so 5547
This theorem is referenced by:  sotric  5574  sotrieq  5575  soirri  6081  suppr  9408  infpr  9440  hartogslem1  9479  canth4  10584  canthwelem  10587  pwfseqlem4  10599  1ne0sr  11033  ltnr  11251  opsrtoslem2  21466  nodenselem4  27038  nodenselem5  27039  nodenselem7  27041  nolt02o  27046  nogt01o  27047  noresle  27048  nosupbnd1lem1  27059  nosupbnd2lem1  27066  noinfbnd1lem1  27074  noinfbnd2lem1  27081  sltirr  27097  fin2solem  36067  fin2so  36068
  Copyright terms: Public domain W3C validator