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 ⁡ ∅