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

Theorem weso 5134
 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 5104 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
21simprbi 479 1 (𝑅 We 𝐴𝑅 Or 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   Or wor 5063   Fr wfr 5099   We wwe 5101 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 5104 This theorem is referenced by:  wecmpep  5135  wetrep  5136  wereu  5139  wereu2  5140  weniso  6644  wexp  7336  wfrlem10  7469  ordunifi  8251  ordtypelem7  8470  ordtypelem8  8471  hartogslem1  8488  wofib  8491  wemapso  8497  oemapso  8617  cantnf  8628  ween  8896  cflim2  9123  fin23lem27  9188  zorn2lem1  9356  zorn2lem4  9359  fpwwe2lem12  9501  fpwwe2lem13  9502  fpwwe2  9503  canth4  9507  canthwelem  9510  pwfseqlem4  9522  ltsopi  9748  wzel  31894  wsuccl  31897  wsuclb  31898  welb  33661  wepwso  37930  fnwe2lem3  37939  wessf1ornlem  39685
 Copyright terms: Public domain W3C validator