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

Theorem ordwe 4404
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 4394 . 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 4114    _E cep 4302    We wwe 4350   Ord word 4390
This theorem is referenced by:  ordfr  4406  trssord  4408  tz7.5  4412  ordelord  4413  tz7.7  4417  epweon  4574  oieu  7249  oiid  7251  hartogslem1  7252  oemapso  7379  cantnf  7390  oemapwe  7391  dfac8b  7653  fin23lem27  7949  om2uzoi  11012  ltweuz  11018  wepwso  26538  onfrALTlem3  27580  onfrALTlem3VD  27931
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 4394
  Copyright terms: Public domain W3C validator