Theorem limensuci

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

	Ref	Expression
Hypothesis	limensuci.1	⊢ Lim 𝐴
Assertion	limensuci	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		limensuci.1	⊢ Lim 𝐴
2	1	limenpsi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ ( 𝐴 ∖ { ∅ } ) )
3	2	ensymd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ { ∅ } ) ≈ 𝐴 )
4		0ex	⊢ ∅ ∈ V
5		en2sn	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → { ∅ } ≈ { 𝐴 } )
6	4 5	mpan	⊢ ( 𝐴 ∈ 𝑉 → { ∅ } ≈ { 𝐴 } )
7		incom	⊢ ( ( 𝐴 ∖ { ∅ } ) ∩ { ∅ } ) = ( { ∅ } ∩ ( 𝐴 ∖ { ∅ } ) )
8		disjdif	⊢ ( { ∅ } ∩ ( 𝐴 ∖ { ∅ } ) ) = ∅
9	7 8	eqtri	⊢ ( ( 𝐴 ∖ { ∅ } ) ∩ { ∅ } ) = ∅
10		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
11	1 10	ax-mp	⊢ Ord 𝐴
12		ordirr	⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
13	11 12	ax-mp	⊢ ¬ 𝐴 ∈ 𝐴
14		disjsn	⊢ ( ( 𝐴 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ 𝐴 )
15	13 14	mpbir	⊢ ( 𝐴 ∩ { 𝐴 } ) = ∅
16		unen	⊢ ( ( ( ( 𝐴 ∖ { ∅ } ) ≈ 𝐴 ∧ { ∅ } ≈ { 𝐴 } ) ∧ ( ( ( 𝐴 ∖ { ∅ } ) ∩ { ∅ } ) = ∅ ∧ ( 𝐴 ∩ { 𝐴 } ) = ∅ ) ) → ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } ) ≈ ( 𝐴 ∪ { 𝐴 } ) )
17	9 15 16	mpanr12	⊢ ( ( ( 𝐴 ∖ { ∅ } ) ≈ 𝐴 ∧ { ∅ } ≈ { 𝐴 } ) → ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } ) ≈ ( 𝐴 ∪ { 𝐴 } ) )
18	3 6 17	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } ) ≈ ( 𝐴 ∪ { 𝐴 } ) )
19		0ellim	⊢ ( Lim 𝐴 → ∅ ∈ 𝐴 )
20	1 19	ax-mp	⊢ ∅ ∈ 𝐴
21	4	snss	⊢ ( ∅ ∈ 𝐴 ↔ { ∅ } ⊆ 𝐴 )
22	20 21	mpbi	⊢ { ∅ } ⊆ 𝐴
23		undif	⊢ ( { ∅ } ⊆ 𝐴 ↔ ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) = 𝐴 )
24	22 23	mpbi	⊢ ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) = 𝐴
25		uncom	⊢ ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) = ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } )
26	24 25	eqtr3i	⊢ 𝐴 = ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } )
27		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
28	18 26 27	3brtr4g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴 )