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	$$⊢\mathrm{Ord}\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		tron	$$⊢\mathrm{Tr}\mathrm{On}$$
2		epweon	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}$$
3		df-ord	$$⊢\mathrm{Ord}\mathrm{On}\leftrightarrow \left(\mathrm{Tr}\mathrm{On}\wedge \mathrm{E}\mathrm{We}\mathrm{On}\right)$$
4	1 2 3	mpbir2an	$$⊢\mathrm{Ord}\mathrm{On}$$