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

Theorem ordwe 4363
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 4353 . 2  |-  ( Ord 
A  <->  ( Tr  A  /\  _E  We  A ) )
21simprbi 452 1  |-  ( Ord 
A  ->  _E  We  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6   Tr wtr 4073    _E cep 4261    We wwe 4309   Ord word 4349
This theorem is referenced by:  ordfr  4365  trssord  4367  tz7.5  4371  ordelord  4372  tz7.7  4376  epweon  4533  oieu  7208  oiid  7210  hartogslem1  7211  oemapso  7338  cantnf  7349  oemapwe  7350  dfac8b  7612  fin23lem27  7908  om2uzoi  10970  ltweuz  10976  wepwso  26492  onfrALTlem3  27346  onfrALTlem3VD  27697
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362  df-ord 4353
  Copyright terms: Public domain W3C validator