Theorem limensuc

Description: A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003)

	Ref	Expression
Assertion	limensuc	$$⊢\left(A\in V\wedge \mathrm{Lim}A\right)\to A\approx \mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to \left(A\in V\leftrightarrow if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\in V\right)$$
2		id	$$⊢A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)$$
3		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)$$
4	2 3	breq12d	$$⊢A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to \left(A\approx \mathrm{suc}A\leftrightarrow if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\approx \mathrm{suc}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\right)$$
5	1 4	imbi12d	$$⊢A=if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\to \left(\left(A\in V\to A\approx \mathrm{suc}A\right)\leftrightarrow \left(if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\in V\to if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\approx \mathrm{suc}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\right)\right)$$
6		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)$$
7		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)$$
8		limon	$$⊢\mathrm{Lim}\mathrm{On}$$
9	6 7 8	elimhyp	$$⊢\mathrm{Lim}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)$$
10	9	limensuci	$$⊢if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\in V\to if\left(\mathrm{Lim}A,A,\mathrm{On}\right)\approx \mathrm{suc}if\left(\mathrm{Lim}A,A,\mathrm{On}\right)$$
11	5 10	dedth	$$⊢\mathrm{Lim}A\to \left(A\in V\to A\approx \mathrm{suc}A\right)$$
12	11	impcom	$$⊢\left(A\in V\wedge \mathrm{Lim}A\right)\to A\approx \mathrm{suc}A$$