Metamath Proof Explorer

Theorem 0ellim

Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994)

Ref Expression
Assertion 0ellim 
|- ( Lim A -> (/) e. A )

Proof

Step Hyp Ref Expression
1 nlim0 
 |-  -. Lim (/)
2 limeq 
 |-  ( A = (/) -> ( Lim A <-> Lim (/) ) )
3 1 2 mtbiri 
 |-  ( A = (/) -> -. Lim A )
4 3 necon2ai 
 |-  ( Lim A -> A =/= (/) )
5 limord 
 |-  ( Lim A -> Ord A )
6 ord0eln0 
 |-  ( Ord A -> ( (/) e. A <-> A =/= (/) ) )
7 5 6 syl 
 |-  ( Lim A -> ( (/) e. A <-> A =/= (/) ) )
8 4 7 mpbird 
 |-  ( Lim A -> (/) e. A )