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

Theorem sopo 4670
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 4654 . 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 964   A.wral 2727   class class class wbr 4304    Po wpo 4651    Or wor 4652
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 4654
This theorem is referenced by:  sonr  4674  sotr  4675  so2nr  4677  so3nr  4678  soltmin  5249  soxp  6697  fimax2g  7570  wofi  7573  ordtypelem8  7751  wemaplem2  7773  wemapsolem  7776  cantnf  7913  cantnfOLD  7935  fin23lem27  8509  iccpnfhmeo  20529  xrhmeo  20530  logccv  22120  ex-po  23654  xrge0iifiso  26377  socnv  27587  predso  27658  soseq  27727  incsequz2  28657
  Copyright terms: Public domain W3C validator