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

Theorem sopo 4817
Description: A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
Assertion
Ref Expression
sopo  |-  ( R  Or  A  ->  R  Po  A )

Proof of Theorem sopo
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-so 4801 . 2  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
21simplbi 460 1  |-  ( R  Or  A  ->  R  Po  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 972   A.wral 2814   class class class wbr 4447    Po wpo 4798    Or wor 4799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-so 4801
This theorem is referenced by:  sonr  4821  sotr  4822  so2nr  4824  so3nr  4825  soltmin  5405  soxp  6896  fimax2g  7765  wofi  7768  ordtypelem8  7949  wemaplem2  7971  wemapsolem  7974  cantnf  8111  cantnfOLD  8133  fin23lem27  8707  iccpnfhmeo  21196  xrhmeo  21197  logccv  22788  ex-po  24849  xrge0iifiso  27569  socnv  28787  predso  28858  soseq  28927  incsequz2  29861
  Copyright terms: Public domain W3C validator