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

Theorem ordwe 5895
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 5885 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simprbi 483 1 (Ord 𝐴 → E We 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4902   E cep 5176   We wwe 5222  Ord word 5881
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 5885
This theorem is referenced by:  ordfr  5897  trssord  5899  tz7.5  5903  ordelord  5904  tz7.7  5908  epweon  7146  oieu  8607  oiid  8609  hartogslem1  8610  oemapso  8750  cantnf  8761  oemapwe  8762  dfac8b  9042  fin23lem27  9340  om2uzoi  12946  ltweuz  12952  wepwso  38113  onfrALTlem3  39259  onfrALTlem3VD  39620
  Copyright terms: Public domain W3C validator