Theorem ordwe 2961

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 2951	. 2 |- (Ord A <-> (Tr A /\ E We A))
2	1	pm3.27bi 326	1 |- (Ord A -> E We A)

Syntax hints:   -> wi 3  Tr wtr 2680  Ecep 2830   We wwe 2916  Ord word 2947

This theorem is referenced by:  ordfr 2963  trssord 2965  tz7.5 2969  ordelord 2970  tz7.7 2973  epweon 2988  weth 4787

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 147  df-an 225  df-ord 2951

Copyright terms: Public domain