Theorem ordwe 6324

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

Syntax hints:   → wi 4  Tr wtr 5202   E cep 5522   We wwe 5575  Ord word 6310

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 6314

This theorem is referenced by:  ordfr  6326  trssord  6328  tz7.5  6332  ordelord  6333  tz7.7  6337  oieu  9450  oiid  9452  hartogslem1  9453  oemapso  9597  cantnf  9608  oemapwe  9609  dfac8b  9944  fin23lem27  10241  om2uzoi  13880  ltweuz  13886  om2noseqoi  28220  wepwso  43019  onfrALTlem3  44521  onfrALTlem3VD  44863