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

Theorem ordwe 4298
Description: Epsilon well orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordwe  |-  ( Ord 
A  ->  _E  We  A )

Proof of Theorem ordwe
StepHypRef Expression
1 df-ord 4288 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simprbi 452 1  |-  ( Ord 
A  ->  _E  We  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6   Tr wtr 4010    _E cep 4196    We wwe 4244   Ord word 4284
This theorem is referenced by:  ordfr  4300  trssord  4302  tz7.5  4306  ordelord  4307  tz7.7  4311  epweon  4466  oieu  7138  oiid  7140  hartogslem1  7141  oemapso  7268  cantnf  7279  oemapwe  7280  dfac8b  7542  fin23lem27  7838  om2uzoi  10896  ltweuz  10902  wepwso  26305  onfrALTlem3  27099  onfrALTlem3VD  27450
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362  df-ord 4288
  Copyright terms: Public domain W3C validator