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

Theorem weso 4870
 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 4840 . 2
21simprbi 464 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wor 4799   wfr 4835   wwe 4837 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 4840 This theorem is referenced by:  wecmpep  4871  wetrep  4872  wereu  4875  wereu2  4876  weniso  6237  wexp  6897  ordunifi  7769  ordtypelem7  7948  ordtypelem8  7949  hartogslem1  7966  wofib  7969  wemapso  7975  oemapso  8100  cantnf  8111  cantnfOLD  8133  ween  8415  cflim2  8642  fin23lem27  8707  zorn2lem1  8875  zorn2lem4  8878  fpwwe2lem12  9018  fpwwe2lem13  9019  fpwwe2  9020  canth4  9024  canthwelem  9027  pwfseqlem4  9039  ltsopi  9265  wfrlem10  28945  wzel  28973  wsuccl  28976  wsuclb  28977  welb  29846  wepwso  30608  fnwe2lem3  30618
 Copyright terms: Public domain W3C validator