MPE Home 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  |-  ( R  We  A  ->  R  Or  A )

Proof of Theorem weso
StepHypRef Expression
1 df-we 4840 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
21simprbi 464 1  |-  ( R  We  A  ->  R  Or  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Or wor 4799    Fr wfr 4835    We 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