Theorem limensuci

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

	Ref	Expression
Hypothesis	limensuci.1	$$⊢\mathrm{Lim}A$$
Assertion	limensuci	$$⊢A\in V\to A\approx \mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		limensuci.1	$$⊢\mathrm{Lim}A$$
2	1	limenpsi	$$⊢A\in V\to A\approx \left(A\setminus \left\{\varnothing \right\}\right)$$
3	2	ensymd	$$⊢A\in V\to \left(A\setminus \left\{\varnothing \right\}\right)\approx A$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5		en2sn	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in V\right)\to \left\{\varnothing \right\}\approx \left\{A\right\}$$
6	4 5	mpan	$$⊢A\in V\to \left\{\varnothing \right\}\approx \left\{A\right\}$$
7		incom	$$⊢\left(A\setminus \left\{\varnothing \right\}\right)\cap \left\{\varnothing \right\}=\left\{\varnothing \right\}\cap \left(A\setminus \left\{\varnothing \right\}\right)$$
8		disjdif	$$⊢\left\{\varnothing \right\}\cap \left(A\setminus \left\{\varnothing \right\}\right)=\varnothing$$
9	7 8	eqtri	$$⊢\left(A\setminus \left\{\varnothing \right\}\right)\cap \left\{\varnothing \right\}=\varnothing$$
10		limord	$$⊢\mathrm{Lim}A\to \mathrm{Ord}A$$
11	1 10	ax-mp	$$⊢\mathrm{Ord}A$$
12		ordirr	$$⊢\mathrm{Ord}A\to \neg A\in A$$
13	11 12	ax-mp	$$⊢\neg A\in A$$
14		disjsn	$$⊢A\cap \left\{A\right\}=\varnothing \leftrightarrow \neg A\in A$$
15	13 14	mpbir	$$⊢A\cap \left\{A\right\}=\varnothing$$
16		unen	$$⊢\left(\left(\left(A\setminus \left\{\varnothing \right\}\right)\approx A\wedge \left\{\varnothing \right\}\approx \left\{A\right\}\right)\wedge \left(\left(A\setminus \left\{\varnothing \right\}\right)\cap \left\{\varnothing \right\}=\varnothing \wedge A\cap \left\{A\right\}=\varnothing \right)\right)\to \left(\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)\approx \left(A\cup \left\{A\right\}\right)$$
17	9 15 16	mpanr12	$$⊢\left(\left(A\setminus \left\{\varnothing \right\}\right)\approx A\wedge \left\{\varnothing \right\}\approx \left\{A\right\}\right)\to \left(\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)\approx \left(A\cup \left\{A\right\}\right)$$
18	3 6 17	syl2anc	$$⊢A\in V\to \left(\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)\approx \left(A\cup \left\{A\right\}\right)$$
19		0ellim	$$⊢\mathrm{Lim}A\to \varnothing \in A$$
20	1 19	ax-mp	$$⊢\varnothing \in A$$
21	4	snss	$$⊢\varnothing \in A\leftrightarrow \left\{\varnothing \right\}\subseteq A$$
22	20 21	mpbi	$$⊢\left\{\varnothing \right\}\subseteq A$$
23		undif	$$⊢\left\{\varnothing \right\}\subseteq A\leftrightarrow \left\{\varnothing \right\}\cup \left(A\setminus \left\{\varnothing \right\}\right)=A$$
24	22 23	mpbi	$$⊢\left\{\varnothing \right\}\cup \left(A\setminus \left\{\varnothing \right\}\right)=A$$
25		uncom	$$⊢\left\{\varnothing \right\}\cup \left(A\setminus \left\{\varnothing \right\}\right)=\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}$$
26	24 25	eqtr3i	$$⊢A=\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}$$
27		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
28	18 26 27	3brtr4g	$$⊢A\in V\to A\approx \mathrm{suc}A$$