This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \leftrightarrow (Tr On \land E We On)$
4	1 2 3	mpbir2an	$⊢ Ord On$