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

Theorem ordwe 5954
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 5944 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simprbi 491 1 (Ord 𝐴 → E We 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4945   E cep 5224   We wwe 5270  Ord word 5940
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 386  df-ord 5944
This theorem is referenced by:  ordfr  5956  trssord  5958  tz7.5  5962  ordelord  5963  tz7.7  5967  oieu  8686  oiid  8688  hartogslem1  8689  oemapso  8829  cantnf  8840  oemapwe  8841  dfac8b  9140  fin23lem27  9438  om2uzoi  13009  ltweuz  13015  wepwso  38394  onfrALTlem3  39526  onfrALTlem3VD  39879
  Copyright terms: Public domain W3C validator