Metamath Proof Explorer


Theorem nlim0

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 (/)

Proof

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 (/)