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

Theorem ordwe 6182
 Description: Membership 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 6172 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simprbi 500 1 (Ord 𝐴 → E We 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Tr wtr 5138   E cep 5434   We wwe 5482  Ord word 6168 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 210  df-an 400  df-ord 6172 This theorem is referenced by:  ordfr  6184  trssord  6186  tz7.5  6190  ordelord  6191  tz7.7  6195  oieu  9036  oiid  9038  hartogslem1  9039  oemapso  9178  cantnf  9189  oemapwe  9190  dfac8b  9491  fin23lem27  9788  om2uzoi  13372  ltweuz  13378  wepwso  40360  onfrALTlem3  41623  onfrALTlem3VD  41966
 Copyright terms: Public domain W3C validator