Theorem ordwe 6378

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

Syntax hints:   → wi 4  Tr wtr 5266   E cep 5580   We wwe 5631  Ord word 6364

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 398  df-ord 6368

This theorem is referenced by:  ordfr  6380  trssord  6382  tz7.5  6386  ordelord  6387  tz7.7  6391  oieu  9534  oiid  9536  hartogslem1  9537  oemapso  9677  cantnf  9688  oemapwe  9689  dfac8b  10026  fin23lem27  10323  om2uzoi  13920  ltweuz  13926  wepwso  41785  onfrALTlem3  43305  onfrALTlem3VD  43648