Metamath Proof Explorer

Theorem limelon

Description: A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004)

Ref Expression
Assertion limelon 
|- ( ( A e. B /\ Lim A ) -> A e. On )

Proof

Step Hyp Ref Expression
1 limord 
 |-  ( Lim A -> Ord A )
2 elong 
 |-  ( A e. B -> ( A e. On <-> Ord A ) )
3 1 2 imbitrrid 
 |-  ( A e. B -> ( Lim A -> A e. On ) )
4 3 imp 
 |-  ( ( A e. B /\ Lim A ) -> A e. On )