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

Theorem sonr 4791
Description: A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
Assertion
Ref Expression
sonr  |-  ( ( R  Or  A  /\  B  e.  A )  ->  -.  B R B )

Proof of Theorem sonr
StepHypRef Expression
1 sopo 4787 . 2  |-  ( R  Or  A  ->  R  Po  A )
2 poirr 4781 . 2  |-  ( ( R  Po  A  /\  B  e.  A )  ->  -.  B R B )
31, 2sylan 473 1  |-  ( ( R  Or  A  /\  B  e.  A )  ->  -.  B R B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370    e. wcel 1868   class class class wbr 4420    Po wpo 4768    Or wor 4769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-po 4770  df-so 4771
This theorem is referenced by:  sotric  4796  sotrieq  4797  soirri  5241  suppr  7989  infpr  8021  hartogslem1  8059  canth4  9072  canthwelem  9075  pwfseqlem4  9087  1ne0sr  9520  ltnr  9728  opsrtoslem2  18695  sltirr  30551  fin2solem  31844  fin2so  31845
  Copyright terms: Public domain W3C validator