Theorem ordwe 5895

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

Syntax hints:   → wi 4  Tr wtr 4902   E cep 5176   We wwe 5222  Ord word 5881

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 385  df-ord 5885

This theorem is referenced by:  ordfr  5897  trssord  5899  tz7.5  5903  ordelord  5904  tz7.7  5908  epweon  7146  oieu  8607  oiid  8609  hartogslem1  8610  oemapso  8750  cantnf  8761  oemapwe  8762  dfac8b  9042  fin23lem27  9340  om2uzoi  12946  ltweuz  12952  wepwso  38113  onfrALTlem3  39259  onfrALTlem3VD  39620