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

Theorem ordwe 5774
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 5764 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simprbi 479 1 (Ord 𝐴 → E We 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4785   E cep 5057   We wwe 5101  Ord word 5760
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-ord 5764
This theorem is referenced by:  ordfr  5776  trssord  5778  tz7.5  5782  ordelord  5783  tz7.7  5787  epweon  7025  oieu  8485  oiid  8487  hartogslem1  8488  oemapso  8617  cantnf  8628  oemapwe  8629  dfac8b  8892  fin23lem27  9188  om2uzoi  12794  ltweuz  12800  wepwso  37930  onfrALTlem3  39076  onfrALTlem3VD  39437
  Copyright terms: Public domain W3C validator