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

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

Proof of Theorem ordwe
StepHypRef Expression
1 df-ord 6072 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simprbi 497 1 (Ord 𝐴 → E We 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 5066   E cep 5355   We wwe 5404  Ord word 6068
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 208  df-an 397  df-ord 6072
This theorem is referenced by:  ordfr  6084  trssord  6086  tz7.5  6090  ordelord  6091  tz7.7  6095  oieu  8852  oiid  8854  hartogslem1  8855  oemapso  8994  cantnf  9005  oemapwe  9006  dfac8b  9306  fin23lem27  9599  om2uzoi  13173  ltweuz  13179  wepwso  39141  onfrALTlem3  40430  onfrALTlem3VD  40773
  Copyright terms: Public domain W3C validator