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

Metamath Proof Explorer

Theorem limon

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

		Ref	Expression
	Assertion	limon	$⊢ Lim On$

Step	Hyp	Ref	Expression
1		ordon	$⊢ Ord On$
2		onn0	$⊢ On \neq \emptyset$
3		unon	$⊢ ⋃ On = On$
4	3	eqcomi	$⊢ On = ⋃ On$
5		df-lim	$⊢ Lim On \leftrightarrow (Ord On \land On \neq \emptyset \land On = ⋃ On)$
6	1 2 4 5	mpbir3an	$⊢ Lim On$