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

Theorem sopo 4792
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 4776 . 2  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
21simplbi 461 1  |-  ( R  Or  A  ->  R  Po  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 981   A.wral 2782   class class class wbr 4426    Po wpo 4773    Or wor 4774
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 188  df-an 372  df-so 4776
This theorem is referenced by:  sonr  4796  sotr  4797  so2nr  4799  so3nr  4800  soltmin  5256  predso  5418  soxp  6920  fimax2g  7823  wofi  7826  ordtypelem8  8040  wemaplem2  8062  wemapsolem  8065  cantnf  8197  fin23lem27  8756  iccpnfhmeo  21869  xrhmeo  21870  logccv  23473  ex-po  25730  xrge0iifiso  28580  socnv  30192  soseq  30279  incsequz2  31782
  Copyright terms: Public domain W3C validator