Theorem ordwe 4896

Description: Epsilon well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordwe

Proof of Theorem ordwe

Step	Hyp	Ref	Expression
1		df-ord 4886	. 2
2	1	simprbi 464	1

Syntax hints:  ->wi 4  Trwtr 4545  cep 4794  Wewwe 4842  Ordword 4882

This theorem is referenced by:  ordfr  4898  trssord  4900  tz7.5  4904  ordelord  4905  tz7.7  4909  epweon  6619  oieu  7985  oiid  7987  hartogslem1  7988  oemapso  8122  cantnf  8133  oemapwe  8134  cantnfOLD  8155  oemapweOLD  8156  dfac8b  8433  fin23lem27  8729  om2uzoi  12066  ltweuz  12072  wepwso  30988  onfrALTlem3  33316  onfrALTlem3VD  33687

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 185  df-an 371  df-ord 4886