Theorem ordwe

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

	Ref	Expression
Assertion	ordwe	⊢ ( Ord 𝐴 → E We 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-ord	⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) )
2	1	simprbi	⊢ ( Ord 𝐴 → E We 𝐴 )