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

Theorem sonr 4775
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 4771 . 2  |-  ( R  Or  A  ->  R  Po  A )
2 poirr 4765 . 2  |-  ( ( R  Po  A  /\  B  e.  A )  ->  -.  B R B )
31, 2sylan 474 1  |-  ( ( R  Or  A  /\  B  e.  A )  ->  -.  B R B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 371    e. wcel 1886   class class class wbr 4401    Po wpo 4752    Or wor 4753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ral 2741  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-po 4754  df-so 4755
This theorem is referenced by:  sotric  4780  sotrieq  4781  soirri  5225  suppr  7984  infpr  8016  hartogslem1  8054  canth4  9069  canthwelem  9072  pwfseqlem4  9084  1ne0sr  9517  ltnr  9725  opsrtoslem2  18701  sltirr  30552  fin2solem  31924  fin2so  31925
  Copyright terms: Public domain W3C validator