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 ∅