Theorem ordwe 2212

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 2202	. 2 ⊢ (Ord A ↔ (Tr A ∧ E We A))
2	1	pm3.27bd 263	1 ⊢ (Ord A → E We A)

Syntax hints:   → wi 2  Tr wtr 2041  Ecep 2056   We wwe 2062  Ord word 2198

This theorem is referenced by:  ordfr 2214  trssord 2216  tz7.5 2220  ordelord 2221  tz7.7 2224  epweon 2239  weth 3602

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-ord 2202

metamath.org