Theorem limon

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

	Ref	Expression
Assertion	limon	⊢ Lim On

Proof

Step	Hyp	Ref	Expression
1		ordon	⊢ Ord On
2		onn0	⊢ On ≠ ∅
3		unon	⊢ ∪ On = On
4	3	eqcomi	⊢ On = ∪ On
5		df-lim	⊢ ( Lim On ↔ ( Ord On ∧ On ≠ ∅ ∧ On = ∪ On ) )
6	1 2 4 5	mpbir3an	⊢ Lim On