Theorem ordwe 6336

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

Step	Hyp	Ref	Expression
1		df-ord 6326	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simprbi 497	1 ⊢ (Ord 𝐴 → E We 𝐴)

Syntax hints:   → wi 4  Tr wtr 5192   E cep 5530   We wwe 5583  Ord word 6322

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 207  df-an 396  df-ord 6326

This theorem is referenced by:  ordfr  6338  trssord  6340  tz7.5  6344  ordelord  6345  tz7.7  6349  oieu  9454  oiid  9456  hartogslem1  9457  oemapso  9603  cantnf  9614  oemapwe  9615  dfac8b  9953  fin23lem27  10250  om2uzoi  13917  ltweuz  13923  om2noseqoi  28295  wepwso  43471  onfrALTlem3  44971  onfrALTlem3VD  45313