Theorem ordwe 6345

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

Syntax hints:   → wi 4  Tr wtr 5214   E cep 5537   We wwe 5590  Ord word 6331

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 6335

This theorem is referenced by:  ordfr  6347  trssord  6349  tz7.5  6353  ordelord  6354  tz7.7  6358  oieu  9492  oiid  9494  hartogslem1  9495  oemapso  9635  cantnf  9646  oemapwe  9647  dfac8b  9984  fin23lem27  10281  om2uzoi  13920  ltweuz  13926  om2noseqoi  28197  wepwso  43032  onfrALTlem3  44534  onfrALTlem3VD  44876