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

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