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 
 |-  U. On = On
4 3 eqcomi 
 |-  On = U. On
5 df-lim 
 |-  ( Lim On <-> ( Ord On /\ On =/= (/) /\ On = U. On ) )
6 1 2 4 5 mpbir3an 
 |-  Lim On