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

Theorem ordwe 5653
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 5643 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simprbi 479 1 (Ord 𝐴 → E We 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 4680   E cep 4947   We wwe 4996  Ord word 5639
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 196  df-an 385  df-ord 5643
This theorem is referenced by:  ordfr  5655  trssord  5657  tz7.5  5661  ordelord  5662  tz7.7  5666  epweon  6875  oieu  8327  oiid  8329  hartogslem1  8330  oemapso  8462  cantnf  8473  oemapwe  8474  dfac8b  8737  fin23lem27  9033  om2uzoi  12616  ltweuz  12622  wepwso  36631  onfrALTlem3  37780  onfrALTlem3VD  38145
  Copyright terms: Public domain W3C validator