Theorem limon

Description: The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995)

	Ref	Expression
Assertion	limon	$$⊢\mathrm{Lim}\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		ordon	$$⊢\mathrm{Ord}\mathrm{On}$$
2		onn0	$$⊢\mathrm{On}\ne \varnothing$$
3		unon	$$⊢\bigcup \mathrm{On}=\mathrm{On}$$
4	3	eqcomi	$$⊢\mathrm{On}=\bigcup \mathrm{On}$$
5		df-lim	$$⊢\mathrm{Lim}\mathrm{On}\leftrightarrow \left(\mathrm{Ord}\mathrm{On}\wedge \mathrm{On}\ne \varnothing \wedge \mathrm{On}=\bigcup \mathrm{On}\right)$$
6	1 2 4 5	mpbir3an	$$⊢\mathrm{Lim}\mathrm{On}$$