Theorem ordon

Description: The class of all ordinal numbers is ordinal. Proposition 7.12 of TakeutiZaring p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994)

	Ref	Expression
Assertion	ordon	|- Ord On

Proof

Step	Hyp	Ref	Expression
1		tron	|- Tr On
2		epweon	|- _E We On
3		df-ord	|- ( Ord On <-> ( Tr On /\ _E We On ) )
4	1 2 3	mpbir2an	|- Ord On