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		disjdifr	$$⊢\left(A\setminus \left\{\varnothing \right\}\right)\cap \left\{\varnothing \right\}=\varnothing$$
8		limord	$$⊢\mathrm{Lim}A\to \mathrm{Ord}A$$
9	1 8	ax-mp	$$⊢\mathrm{Ord}A$$
10		ordirr	$$⊢\mathrm{Ord}A\to \neg A\in A$$
11	9 10	ax-mp	$$⊢\neg A\in A$$
12		disjsn	$$⊢A\cap \left\{A\right\}=\varnothing \leftrightarrow \neg A\in A$$
13	11 12	mpbir	$$⊢A\cap \left\{A\right\}=\varnothing$$
14		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)$$
15	7 13 14	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)$$
16	3 6 15	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)$$
17		0ellim	$$⊢\mathrm{Lim}A\to \varnothing \in A$$
18	1 17	ax-mp	$$⊢\varnothing \in A$$
19	4	snss	$$⊢\varnothing \in A\leftrightarrow \left\{\varnothing \right\}\subseteq A$$
20	18 19	mpbi	$$⊢\left\{\varnothing \right\}\subseteq A$$
21		undif	$$⊢\left\{\varnothing \right\}\subseteq A\leftrightarrow \left\{\varnothing \right\}\cup \left(A\setminus \left\{\varnothing \right\}\right)=A$$
22	20 21	mpbi	$$⊢\left\{\varnothing \right\}\cup \left(A\setminus \left\{\varnothing \right\}\right)=A$$
23		uncom	$$⊢\left\{\varnothing \right\}\cup \left(A\setminus \left\{\varnothing \right\}\right)=\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}$$
24	22 23	eqtr3i	$$⊢A=\left(A\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}$$
25		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
26	16 24 25	3brtr4g	$$⊢A\in V\to A\approx \mathrm{suc}A$$