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		dflim2	$$⊢\mathrm{Lim}A\leftrightarrow \left(\mathrm{Ord}A\wedge \varnothing \in A\wedge A=\bigcup A\right)$$
2	1	simp2bi	$$⊢\mathrm{Lim}A\to \varnothing \in A$$