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

Theorem ordwe 4586
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 4576 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simprbi 451 1  |-  ( Ord 
A  ->  _E  We  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Tr wtr 4294    _E cep 4484    We wwe 4532   Ord word 4572
This theorem is referenced by:  ordfr  4588  trssord  4590  tz7.5  4594  ordelord  4595  tz7.7  4599  epweon  4755  oieu  7497  oiid  7499  hartogslem1  7500  oemapso  7627  cantnf  7638  oemapwe  7639  dfac8b  7901  fin23lem27  8197  om2uzoi  11283  ltweuz  11289  wepwso  27054  onfrALTlem3  28485  onfrALTlem3VD  28853
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-ord 4576
  Copyright terms: Public domain W3C validator