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

Theorem sopo 4462
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 4446 . 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 2650   class class class wbr 4154    Po wpo 4443    Or wor 4444
This theorem is referenced by:  sonr  4466  sotr  4467  so2nr  4469  so3nr  4470  soltmin  5214  soxp  6396  fimax2g  7290  wofi  7293  ordtypelem8  7428  wemaplem2  7450  wemapso2lem  7453  cantnf  7583  fin23lem27  8142  iccpnfhmeo  18842  xrhmeo  18843  logccv  20422  ex-po  21592  xrge0iifiso  24126  predso  25210  soseq  25279  incsequz2  26145
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 4446
  Copyright terms: Public domain W3C validator