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 )