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

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

Proof of Theorem weso
StepHypRef Expression
1 df-we 5227 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simprbi 483 1 (𝑅 We 𝐴𝑅 Or 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Or wor 5186   Fr wfr 5222   We wwe 5224
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 197  df-an 385  df-we 5227
This theorem is referenced by:  wecmpep  5258  wetrep  5259  wereu  5262  wereu2  5263  weniso  6767  wexp  7459  wfrlem10  7593  ordunifi  8375  ordtypelem7  8594  ordtypelem8  8595  hartogslem1  8612  wofib  8615  wemapso  8621  oemapso  8752  cantnf  8763  ween  9048  cflim2  9277  fin23lem27  9342  zorn2lem1  9510  zorn2lem4  9513  fpwwe2lem12  9655  fpwwe2lem13  9656  fpwwe2  9657  canth4  9661  canthwelem  9664  pwfseqlem4  9676  ltsopi  9902  wzel  32075  wsuccl  32078  wsuclb  32079  welb  33844  wepwso  38115  fnwe2lem3  38124  wessf1ornlem  39870
  Copyright terms: Public domain W3C validator