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

Theorem sopo 4822
Description: A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
Assertion
Ref Expression
sopo

Proof of Theorem sopo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-so 4806 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/w3o 972  A.wral 2807   class class class wbr 4452  Powpo 4803  Orwor 4804
This theorem is referenced by:  sonr  4826  sotr  4827  so2nr  4829  so3nr  4830  soltmin  5411  soxp  6913  fimax2g  7786  wofi  7789  ordtypelem8  7971  wemaplem2  7993  wemapsolem  7996  cantnf  8133  cantnfOLD  8155  fin23lem27  8729  iccpnfhmeo  21445  xrhmeo  21446  logccv  23044  ex-po  25156  xrge0iifiso  27917  socnv  29194  predso  29265  soseq  29334  incsequz2  30242
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 4806
  Copyright terms: Public domain W3C validator