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	$$⊢\neg \mathrm{Lim}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg \varnothing \in \varnothing$$
2		simp2	$$⊢\left(\mathrm{Ord}\varnothing \wedge \varnothing \in \varnothing \wedge \varnothing =\bigcup \varnothing \right)\to \varnothing \in \varnothing$$
3	1 2	mto	$$⊢\neg \left(\mathrm{Ord}\varnothing \wedge \varnothing \in \varnothing \wedge \varnothing =\bigcup \varnothing \right)$$
4		dflim2	$$⊢\mathrm{Lim}\varnothing \leftrightarrow \left(\mathrm{Ord}\varnothing \wedge \varnothing \in \varnothing \wedge \varnothing =\bigcup \varnothing \right)$$
5	3 4	mtbir	$$⊢\neg \mathrm{Lim}\varnothing$$