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

Theorem ordwe 5698
Description: Epsilon well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordwe (Ord 𝐴 → E We 𝐴)

Proof of Theorem ordwe
StepHypRef Expression
1 df-ord 5688 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simprbi 480 1 (Ord 𝐴 → E We 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4717   E cep 4988   We wwe 5037  Ord word 5684
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 197  df-an 386  df-ord 5688
This theorem is referenced by:  ordfr  5700  trssord  5702  tz7.5  5706  ordelord  5707  tz7.7  5711  epweon  6931  oieu  8389  oiid  8391  hartogslem1  8392  oemapso  8524  cantnf  8535  oemapwe  8536  dfac8b  8799  fin23lem27  9095  om2uzoi  12691  ltweuz  12697  wepwso  37079  onfrALTlem3  38227  onfrALTlem3VD  38592
  Copyright terms: Public domain W3C validator