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

Theorem sopo 4347
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 4331 . 2  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
21simplbi 446 1  |-  ( R  Or  A  ->  R  Po  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 933    = wceq 1632   A.wral 2556   class class class wbr 4039    Po wpo 4328    Or wor 4329
This theorem is referenced by:  sonr  4351  sotr  4352  so2nr  4354  so3nr  4355  soltmin  5098  soxp  6244  fimax2g  7119  wofi  7122  ordtypelem8  7256  wemaplem2  7278  wemapso2lem  7281  cantnf  7411  fin23lem27  7970  iccpnfhmeo  18459  xrhmeo  18460  logccv  20026  ex-po  20838  xrge0iifiso  23332  predso  24256  soseq  24325  incsequz2  26562
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 177  df-an 360  df-so 4331
  Copyright terms: Public domain W3C validator