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

Theorem ordwe 4822
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 4812 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simprbi 462 1  |-  ( Ord 
A  ->  _E  We  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Tr wtr 4477    _E cep 4720    We wwe 4768   Ord word 4808
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 185  df-an 369  df-ord 4812
This theorem is referenced by:  ordfr  4824  trssord  4826  tz7.5  4830  ordelord  4831  tz7.7  4835  epweon  6540  oieu  7901  oiid  7903  hartogslem1  7904  oemapso  8036  cantnf  8047  oemapwe  8048  cantnfOLD  8069  oemapweOLD  8070  dfac8b  8347  fin23lem27  8643  om2uzoi  11992  ltweuz  11998  wepwso  31194  onfrALTlem3  33695  onfrALTlem3VD  34073
  Copyright terms: Public domain W3C validator