Theorem nnlim

Description: A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995)

	Ref	Expression
Assertion	nnlim	$$⊢A\in \mathrm{\omega }\to \neg \mathrm{Lim}A$$

Proof

Step	Hyp	Ref	Expression
1		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
2		ordirr	$$⊢\mathrm{Ord}A\to \neg A\in A$$
3	1 2	syl	$$⊢A\in \mathrm{\omega }\to \neg A\in A$$
4		elom	$$⊢A\in \mathrm{\omega }\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\left(\mathrm{Lim}x\to A\in x\right)\right)$$
5	4	simprbi	$$⊢A\in \mathrm{\omega }\to \forall x\left(\mathrm{Lim}x\to A\in x\right)$$
6		limeq	$$⊢x=A\to \left(\mathrm{Lim}x\leftrightarrow \mathrm{Lim}A\right)$$
7		eleq2	$$⊢x=A\to \left(A\in x\leftrightarrow A\in A\right)$$
8	6 7	imbi12d	$$⊢x=A\to \left(\left(\mathrm{Lim}x\to A\in x\right)\leftrightarrow \left(\mathrm{Lim}A\to A\in A\right)\right)$$
9	8	spcgv	$$⊢A\in \mathrm{\omega }\to \left(\forall x\left(\mathrm{Lim}x\to A\in x\right)\to \left(\mathrm{Lim}A\to A\in A\right)\right)$$
10	5 9	mpd	$$⊢A\in \mathrm{\omega }\to \left(\mathrm{Lim}A\to A\in A\right)$$
11	3 10	mtod	$$⊢A\in \mathrm{\omega }\to \neg \mathrm{Lim}A$$