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