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

Theorem weso 4709
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 4679 . 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 4638    Fr wfr 4674    We wwe 4676
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 4679
This theorem is referenced by:  wecmpep  4710  wetrep  4711  wereu  4714  wereu2  4715  weniso  6043  wexp  6684  ordunifi  7560  ordtypelem7  7736  ordtypelem8  7737  hartogslem1  7754  wofib  7757  wemapso  7763  oemapso  7888  cantnf  7899  cantnfOLD  7921  ween  8203  cflim2  8430  fin23lem27  8495  zorn2lem1  8663  zorn2lem4  8666  fpwwe2lem12  8806  fpwwe2lem13  8807  fpwwe2  8808  canth4  8812  canthwelem  8815  pwfseqlem4  8827  ltsopi  9055  wfrlem10  27731  wzel  27759  wsuccl  27762  wsuclb  27763  welb  28627  wepwso  29392  fnwe2lem3  29402
  Copyright terms: Public domain W3C validator