Theorem ordwe 3671

Description: Epsilon well orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36.

Assertion

Ref	Expression
ordwe	|- (Ord A -> _E We A)

Proof of Theorem ordwe

Step	Hyp	Ref	Expression
1		df-ord 3660	. 2 |- (Ord A <-> (Tr A /\ _E We A))
2	1	simprbi 353	1 |- (Ord A -> _E We A)

Syntax hints:   -> wi 3  Tr wtr 3411   _E cep 3581   We wwe 3624  Ord word 3656

This theorem is referenced by:  ordfr 3673  trssord 3675  tz7.5 3679  ordelord 3680  tz7.7 3684  epweon 3864  hartog 5693  weth 5949  hartogOLD 15384

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-ord 3660

Copyright terms: Public domain