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

Theorem sopo 4512
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 4496 . 2  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
21simplbi 447 1  |-  ( R  Or  A  ->  R  Po  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 935   A.wral 2697   class class class wbr 4204    Po wpo 4493    Or wor 4494
This theorem is referenced by:  sonr  4516  sotr  4517  so2nr  4519  so3nr  4520  soltmin  5265  soxp  6451  fimax2g  7345  wofi  7348  ordtypelem8  7486  wemaplem2  7508  wemapso2lem  7511  cantnf  7641  fin23lem27  8200  iccpnfhmeo  18962  xrhmeo  18963  logccv  20546  ex-po  21735  xrge0iifiso  24313  socnv  25380  predso  25452  soseq  25521  incsequz2  26434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-so 4496
  Copyright terms: Public domain W3C validator