Description: The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | nlim0 | |- -. Lim (/) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel | |- -. (/) e. (/) |
|
2 | simp2 | |- ( ( Ord (/) /\ (/) e. (/) /\ (/) = U. (/) ) -> (/) e. (/) ) |
|
3 | 1 2 | mto | |- -. ( Ord (/) /\ (/) e. (/) /\ (/) = U. (/) ) |
4 | dflim2 | |- ( Lim (/) <-> ( Ord (/) /\ (/) e. (/) /\ (/) = U. (/) ) ) |
|
5 | 3 4 | mtbir | |- -. Lim (/) |