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

Theorem weso 4875
Description: A well-ordering is a strict ordering. (Contributed by NM, 16-Mar-1997.)
Assertion
Ref Expression
weso

Proof of Theorem weso
StepHypRef Expression
1 df-we 4845 . 2
21simprbi 464 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  Orwor 4804  Frwfr 4840  Wewwe 4842
This theorem is referenced by:  wecmpep  4876  wetrep  4877  wereu  4880  wereu2  4881  weniso  6250  wexp  6914  ordunifi  7790  ordtypelem7  7970  ordtypelem8  7971  hartogslem1  7988  wofib  7991  wemapso  7997  oemapso  8122  cantnf  8133  cantnfOLD  8155  ween  8437  cflim2  8664  fin23lem27  8729  zorn2lem1  8897  zorn2lem4  8900  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  canth4  9046  canthwelem  9049  pwfseqlem4  9061  ltsopi  9287  wfrlem10  29352  wzel  29380  wsuccl  29383  wsuclb  29384  welb  30227  wepwso  30988  fnwe2lem3  30998
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-we 4845
  Copyright terms: Public domain W3C validator