Theorem ordwe 6338

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 6328	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simprbi 497	1 ⊢ (Ord 𝐴 → E We 𝐴)

Syntax hints:   → wi 4  Tr wtr 5207   E cep 5531   We wwe 5584  Ord word 6324

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 6328

This theorem is referenced by:  ordfr  6340  trssord  6342  tz7.5  6346  ordelord  6347  tz7.7  6351  oieu  9456  oiid  9458  hartogslem1  9459  oemapso  9603  cantnf  9614  oemapwe  9615  dfac8b  9953  fin23lem27  10250  om2uzoi  13890  ltweuz  13896  om2noseqoi  28311  wepwso  43397  onfrALTlem3  44897  onfrALTlem3VD  45239