Theorem ordwe 5954

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

Syntax hints:   → wi 4  Tr wtr 4945   E cep 5224   We wwe 5270  Ord word 5940

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 199  df-an 386  df-ord 5944

This theorem is referenced by:  ordfr  5956  trssord  5958  tz7.5  5962  ordelord  5963  tz7.7  5967  oieu  8686  oiid  8688  hartogslem1  8689  oemapso  8829  cantnf  8840  oemapwe  8841  dfac8b  9140  fin23lem27  9438  om2uzoi  13009  ltweuz  13015  wepwso  38394  onfrALTlem3  39526  onfrALTlem3VD  39879