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

Theorem ordwe 4405
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 4395 . 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 4113    _E cep 4303    We wwe 4351   Ord word 4391
This theorem is referenced by:  ordfr  4407  trssord  4409  tz7.5  4413  ordelord  4414  tz7.7  4418  epweon  4575  oieu  7254  oiid  7256  hartogslem1  7257  oemapso  7384  cantnf  7395  oemapwe  7396  dfac8b  7658  fin23lem27  7954  om2uzoi  11018  ltweuz  11024  wepwso  27139  onfrALTlem3  28309  onfrALTlem3VD  28663
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 4395
  Copyright terms: Public domain W3C validator