Theorem limensuci

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

	Ref	Expression
Hypothesis	limensuci.1	|- Lim A
Assertion	limensuci	|- ( A e. V -> A ~~ suc A )

Proof

Step	Hyp	Ref	Expression
1		limensuci.1	|- Lim A
2	1	limenpsi	|- ( A e. V -> A ~~ ( A \ { (/) } ) )
3	2	ensymd	|- ( A e. V -> ( A \ { (/) } ) ~~ A )
4		0ex	|- (/) e. _V
5		en2sn	|- ( ( (/) e. _V /\ A e. V ) -> { (/) } ~~ { A } )
6	4 5	mpan	|- ( A e. V -> { (/) } ~~ { A } )
7		incom	|- ( ( A \ { (/) } ) i^i { (/) } ) = ( { (/) } i^i ( A \ { (/) } ) )
8		disjdif	|- ( { (/) } i^i ( A \ { (/) } ) ) = (/)
9	7 8	eqtri	|- ( ( A \ { (/) } ) i^i { (/) } ) = (/)
10		limord	|- ( Lim A -> Ord A )
11	1 10	ax-mp	|- Ord A
12		ordirr	|- ( Ord A -> -. A e. A )
13	11 12	ax-mp	|- -. A e. A
14		disjsn	|- ( ( A i^i { A } ) = (/) <-> -. A e. A )
15	13 14	mpbir	|- ( A i^i { A } ) = (/)
16		unen	|- ( ( ( ( A \ { (/) } ) ~~ A /\ { (/) } ~~ { A } ) /\ ( ( ( A \ { (/) } ) i^i { (/) } ) = (/) /\ ( A i^i { A } ) = (/) ) ) -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
17	9 15 16	mpanr12	|- ( ( ( A \ { (/) } ) ~~ A /\ { (/) } ~~ { A } ) -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
18	3 6 17	syl2anc	|- ( A e. V -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
19		0ellim	|- ( Lim A -> (/) e. A )
20	1 19	ax-mp	|- (/) e. A
21	4	snss	|- ( (/) e. A <-> { (/) } C_ A )
22	20 21	mpbi	|- { (/) } C_ A
23		undif	|- ( { (/) } C_ A <-> ( { (/) } u. ( A \ { (/) } ) ) = A )
24	22 23	mpbi	|- ( { (/) } u. ( A \ { (/) } ) ) = A
25		uncom	|- ( { (/) } u. ( A \ { (/) } ) ) = ( ( A \ { (/) } ) u. { (/) } )
26	24 25	eqtr3i	|- A = ( ( A \ { (/) } ) u. { (/) } )
27		df-suc	|- suc A = ( A u. { A } )
28	18 26 27	3brtr4g	|- ( A e. V -> A ~~ suc A )