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

Theorem ordwe 6366
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 6356 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
21simprbi 497 1 (Ord 𝐴 → E We 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Tr wtr 5258   E cep 5572   We wwe 5623  Ord word 6352
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 206  df-an 397  df-ord 6356
This theorem is referenced by:  ordfr  6368  trssord  6370  tz7.5  6374  ordelord  6375  tz7.7  6379  oieu  9516  oiid  9518  hartogslem1  9519  oemapso  9659  cantnf  9670  oemapwe  9671  dfac8b  10008  fin23lem27  10305  om2uzoi  13902  ltweuz  13908  wepwso  41554  onfrALTlem3  43074  onfrALTlem3VD  43417
  Copyright terms: Public domain W3C validator