Theorem limsucncmp

Description: The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015)

	Ref	Expression
Assertion	limsucncmp	$$⊢\mathrm{Lim}A\to \neg \mathrm{suc}A\in \mathrm{Comp}$$

Proof

Step	Hyp	Ref	Expression
1		suceq	$$⊢A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to \mathrm{suc}A=\mathrm{suc}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)$$
2	1	eleq1d	$$⊢A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to \left(\mathrm{suc}A\in \mathrm{Comp}\leftrightarrow \mathrm{suc}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\in \mathrm{Comp}\right)$$
3	2	notbid	$$⊢A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to \left(\neg \mathrm{suc}A\in \mathrm{Comp}\leftrightarrow \neg \mathrm{suc}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\in \mathrm{Comp}\right)$$
4		limeq	$$⊢A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to \left(\mathrm{Lim}A\leftrightarrow \mathrm{Lim}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\right)$$
5		limeq	$$⊢\mathrm{On}=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to \left(\mathrm{Lim}\mathrm{On}\leftrightarrow \mathrm{Lim}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\right)$$
6		limon	$$⊢\mathrm{Lim}\mathrm{On}$$
7	4 5 6	elimhyp	$$⊢\mathrm{Lim}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)$$
8	7	limsucncmpi	$$⊢\neg \mathrm{suc}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\in \mathrm{Comp}$$
9	3 8	dedth	$$⊢\mathrm{Lim}A\to \neg \mathrm{suc}A\in \mathrm{Comp}$$