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		disjdifr	|- ( ( A \ { (/) } ) i^i { (/) } ) = (/)
8		limord	|- ( Lim A -> Ord A )
9	1 8	ax-mp	|- Ord A
10		ordirr	|- ( Ord A -> -. A e. A )
11	9 10	ax-mp	|- -. A e. A
12		disjsn	|- ( ( A i^i { A } ) = (/) <-> -. A e. A )
13	11 12	mpbir	|- ( A i^i { A } ) = (/)
14		unen	|- ( ( ( ( A \ { (/) } ) ~~ A /\ { (/) } ~~ { A } ) /\ ( ( ( A \ { (/) } ) i^i { (/) } ) = (/) /\ ( A i^i { A } ) = (/) ) ) -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
15	7 13 14	mpanr12	|- ( ( ( A \ { (/) } ) ~~ A /\ { (/) } ~~ { A } ) -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
16	3 6 15	syl2anc	|- ( A e. V -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
17		0ellim	|- ( Lim A -> (/) e. A )
18	1 17	ax-mp	|- (/) e. A
19	4	snss	|- ( (/) e. A <-> { (/) } C_ A )
20	18 19	mpbi	|- { (/) } C_ A
21		undif	|- ( { (/) } C_ A <-> ( { (/) } u. ( A \ { (/) } ) ) = A )
22	20 21	mpbi	|- ( { (/) } u. ( A \ { (/) } ) ) = A
23		uncom	|- ( { (/) } u. ( A \ { (/) } ) ) = ( ( A \ { (/) } ) u. { (/) } )
24	22 23	eqtr3i	|- A = ( ( A \ { (/) } ) u. { (/) } )
25		df-suc	|- suc A = ( A u. { A } )
26	16 24 25	3brtr4g	|- ( A e. V -> A ~~ suc A )