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

Theorem ordwe 4421
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 4411 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simprbi 450 1  |-  ( Ord 
A  ->  _E  We  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Tr wtr 4129    _E cep 4319    We wwe 4367   Ord word 4407
This theorem is referenced by:  ordfr  4423  trssord  4425  tz7.5  4429  ordelord  4430  tz7.7  4434  epweon  4591  oieu  7270  oiid  7272  hartogslem1  7273  oemapso  7400  cantnf  7411  oemapwe  7412  dfac8b  7674  fin23lem27  7970  om2uzoi  11034  ltweuz  11040  wepwso  27242  onfrALTlem3  28608  onfrALTlem3VD  28979
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 177  df-an 360  df-ord 4411
  Copyright terms: Public domain W3C validator