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

Theorem ordwe 4896
Description: Epsilon well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordwe

Proof of Theorem ordwe
StepHypRef Expression
1 df-ord 4886 . 2
21simprbi 464 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  Trwtr 4545   cep 4794  Wewwe 4842  Ordword 4882
This theorem is referenced by:  ordfr  4898  trssord  4900  tz7.5  4904  ordelord  4905  tz7.7  4909  epweon  6619  oieu  7985  oiid  7987  hartogslem1  7988  oemapso  8122  cantnf  8133  oemapwe  8134  cantnfOLD  8155  oemapweOLD  8156  dfac8b  8433  fin23lem27  8729  om2uzoi  12066  ltweuz  12072  wepwso  30988  onfrALTlem3  33316  onfrALTlem3VD  33687
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-ord 4886
  Copyright terms: Public domain W3C validator