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

Theorem weso 5398
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 5368 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simprbi 489 1 (𝑅 We 𝐴𝑅 Or 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Or wor 5325   Fr wfr 5363   We wwe 5365
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 199  df-an 388  df-we 5368
This theorem is referenced by:  wecmpep  5399  wetrep  5400  wereu  5403  wereu2  5404  weniso  6930  wexp  7629  wfrlem10  7768  ordunifi  8563  ordtypelem7  8783  ordtypelem8  8784  hartogslem1  8801  wofib  8804  wemapso  8810  oemapso  8939  cantnf  8950  ween  9255  cflim2  9483  fin23lem27  9548  zorn2lem1  9716  zorn2lem4  9719  fpwwe2lem12  9861  fpwwe2lem13  9862  fpwwe2  9863  canth4  9867  canthwelem  9870  pwfseqlem4  9882  ltsopi  10108  wzel  32629  wsuccl  32632  wsuclb  32633  welb  34450  wepwso  39036  fnwe2lem3  39045  wessf1ornlem  40867
  Copyright terms: Public domain W3C validator