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

Theorem sopo 4331
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 4315 . 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 1623   A.wral 2543   class class class wbr 4023    Po wpo 4312    Or wor 4313
This theorem is referenced by:  sonr  4335  sotr  4336  so2nr  4338  so3nr  4339  soltmin  5082  soxp  6228  fimax2g  7103  wofi  7106  ordtypelem8  7240  wemaplem2  7262  wemapso2lem  7265  cantnf  7395  fin23lem27  7954  iccpnfhmeo  18443  xrhmeo  18444  logccv  20010  ex-po  20822  xrge0iifiso  23317  predso  24185  soseq  24254  incsequz2  26459
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 4315
  Copyright terms: Public domain W3C validator