Theorem nlimsucg

Description: A successor is not a limit ordinal. (Contributed by NM, 25-Mar-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	nlimsucg	$$⊢A\in V\to \neg \mathrm{Lim}\mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		limord	$$⊢\mathrm{Lim}\mathrm{suc}A\to \mathrm{Ord}\mathrm{suc}A$$
2		ordsuc	$$⊢\mathrm{Ord}A\leftrightarrow \mathrm{Ord}\mathrm{suc}A$$
3	1 2	sylibr	$$⊢\mathrm{Lim}\mathrm{suc}A\to \mathrm{Ord}A$$
4		limuni	$$⊢\mathrm{Lim}\mathrm{suc}A\to \mathrm{suc}A=\bigcup \mathrm{suc}A$$
5		ordunisuc	$$⊢\mathrm{Ord}A\to \bigcup \mathrm{suc}A=A$$
6	5	eqeq2d	$$⊢\mathrm{Ord}A\to \left(\mathrm{suc}A=\bigcup \mathrm{suc}A\leftrightarrow \mathrm{suc}A=A\right)$$
7		ordirr	$$⊢\mathrm{Ord}A\to \neg A\in A$$
8		eleq2	$$⊢\mathrm{suc}A=A\to \left(A\in \mathrm{suc}A\leftrightarrow A\in A\right)$$
9	8	notbid	$$⊢\mathrm{suc}A=A\to \left(\neg A\in \mathrm{suc}A\leftrightarrow \neg A\in A\right)$$
10	7 9	syl5ibrcom	$$⊢\mathrm{Ord}A\to \left(\mathrm{suc}A=A\to \neg A\in \mathrm{suc}A\right)$$
11		sucidg	$$⊢A\in V\to A\in \mathrm{suc}A$$
12	11	con3i	$$⊢\neg A\in \mathrm{suc}A\to \neg A\in V$$
13	10 12	syl6	$$⊢\mathrm{Ord}A\to \left(\mathrm{suc}A=A\to \neg A\in V\right)$$
14	6 13	sylbid	$$⊢\mathrm{Ord}A\to \left(\mathrm{suc}A=\bigcup \mathrm{suc}A\to \neg A\in V\right)$$
15	3 4 14	sylc	$$⊢\mathrm{Lim}\mathrm{suc}A\to \neg A\in V$$
16	15	con2i	$$⊢A\in V\to \neg \mathrm{Lim}\mathrm{suc}A$$