Theorem ordwe 5736

Description: Epsilon 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 5726	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simprbi 480	1 ⊢ (Ord 𝐴 → E We 𝐴)

Syntax hints:   → wi 4  Tr wtr 4752   E cep 5028   We wwe 5072  Ord word 5722

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 197  df-an 386  df-ord 5726

This theorem is referenced by:  ordfr  5738  trssord  5740  tz7.5  5744  ordelord  5745  tz7.7  5749  epweon  6983  oieu  8444  oiid  8446  hartogslem1  8447  oemapso  8579  cantnf  8590  oemapwe  8591  dfac8b  8854  fin23lem27  9150  om2uzoi  12754  ltweuz  12760  wepwso  37613  onfrALTlem3  38759  onfrALTlem3VD  39123