This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ¬ ∅ ∈ ∅
2 simp2 ⊢ ( ( Ord ∅ ∧ ∅ ∈ ∅ ∧ ∅ = ∪ ∅ ) → ∅ ∈ ∅ )
3 1 2 mto ⊢ ¬ ( Ord ∅ ∧ ∅ ∈ ∅ ∧ ∅ = ∪ ∅ )
4 dflim2 ⊢ ( Lim ∅ ↔ ( Ord ∅ ∧ ∅ ∈ ∅ ∧ ∅ = ∪ ∅ ) )
5 3 4 mtbir ⊢ ¬ Lim ∅