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

Theorem ordwe 4843
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 4833 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simprbi 464 1  |-  ( Ord 
A  ->  _E  We  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Tr wtr 4496    _E cep 4741    We wwe 4789   Ord word 4829
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 371  df-ord 4833
This theorem is referenced by:  ordfr  4845  trssord  4847  tz7.5  4851  ordelord  4852  tz7.7  4856  epweon  6508  oieu  7867  oiid  7869  hartogslem1  7870  oemapso  8004  cantnf  8015  oemapwe  8016  cantnfOLD  8037  oemapweOLD  8038  dfac8b  8315  fin23lem27  8611  om2uzoi  11898  ltweuz  11904  wepwso  29563  onfrALTlem3  31604  onfrALTlem3VD  31975
  Copyright terms: Public domain W3C validator