Theorem 0ellim

Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994)

	Ref	Expression
Assertion	0ellim	$$⊢\mathrm{Lim}A\to \varnothing \in A$$

Proof

Step	Hyp	Ref	Expression
1		nlim0	$$⊢\neg \mathrm{Lim}\varnothing$$
2		limeq	$$⊢A=\varnothing \to \left(\mathrm{Lim}A\leftrightarrow \mathrm{Lim}\varnothing \right)$$
3	1 2	mtbiri	$$⊢A=\varnothing \to \neg \mathrm{Lim}A$$
4	3	necon2ai	$$⊢\mathrm{Lim}A\to A\ne \varnothing$$
5		limord	$$⊢\mathrm{Lim}A\to \mathrm{Ord}A$$
6		ord0eln0	$$⊢\mathrm{Ord}A\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$
7	5 6	syl	$$⊢\mathrm{Lim}A\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$
8	4 7	mpbird	$$⊢\mathrm{Lim}A\to \varnothing \in A$$