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