Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | 0ellim | |- ( Lim A -> (/) e. A ) |
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 ) |